let U be Subset of REAL; :: thesis: { x where x is Element of REAL : x is_local_minimum_of U } is countable

set X = { x where x is Element of REAL : x is_local_minimum_of U } ;

defpred S_{1}[ object , object ] means ex x, y being Real st

( $1 = x & $2 = ].y,x.[ & y < x & ].y,x.[ misses U );

A4: ( dom f = { x where x is Element of REAL : x is_local_minimum_of U } & rng f c= bool REAL ) and

A5: for a being object st a in { x where x is Element of REAL : x is_local_minimum_of U } holds

S_{1}[a,f . a]
from FUNCT_1:sch 6(A1);

f is one-to-one

A24: rng f is mutually-disjoint

then card (rng f) c= omega ;

hence card { x where x is Element of REAL : x is_local_minimum_of U } c= omega by A23; :: according to CARD_3:def 14 :: thesis: verum

set X = { x where x is Element of REAL : x is_local_minimum_of U } ;

defpred S

( $1 = x & $2 = ].y,x.[ & y < x & ].y,x.[ misses U );

A1: now :: thesis: for a being object st a in { x where x is Element of REAL : x is_local_minimum_of U } holds

ex b being object st

( b in bool REAL & S_{1}[a,b] )

consider f being Function such that ex b being object st

( b in bool REAL & S

let a be object ; :: thesis: ( a in { x where x is Element of REAL : x is_local_minimum_of U } implies ex b being object st

( b in bool REAL & S_{1}[a,b] ) )

assume a in { x where x is Element of REAL : x is_local_minimum_of U } ; :: thesis: ex b being object st

( b in bool REAL & S_{1}[a,b] )

then consider x being Element of REAL such that

A2: a = x and

A3: x is_local_minimum_of U ;

ex y being Real st

( y < x & ].y,x.[ misses U ) by A3;

hence ex b being object st

( b in bool REAL & S_{1}[a,b] )
by A2; :: thesis: verum

end;( b in bool REAL & S

assume a in { x where x is Element of REAL : x is_local_minimum_of U } ; :: thesis: ex b being object st

( b in bool REAL & S

then consider x being Element of REAL such that

A2: a = x and

A3: x is_local_minimum_of U ;

ex y being Real st

( y < x & ].y,x.[ misses U ) by A3;

hence ex b being object st

( b in bool REAL & S

A4: ( dom f = { x where x is Element of REAL : x is_local_minimum_of U } & rng f c= bool REAL ) and

A5: for a being object st a in { x where x is Element of REAL : x is_local_minimum_of U } holds

S

f is one-to-one

proof

then A23:
card { x where x is Element of REAL : x is_local_minimum_of U } c= card (rng f)
by A4, CARD_1:10;
let a9, b9 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a9 in dom f or not b9 in dom f or not f . a9 = f . b9 or a9 = b9 )

set a = f . a9;

set b = f . b9;

assume that

A6: a9 in dom f and

A7: b9 in dom f ; :: thesis: ( not f . a9 = f . b9 or a9 = b9 )

consider xb, yb being Real such that

A8: b9 = xb and

A9: f . b9 = ].yb,xb.[ and

yb < xb and

A10: ].yb,xb.[ misses U by A4, A5, A7;

ex x being Element of REAL st

( xb = x & x is_local_minimum_of U ) by A4, A7, A8;

then A11: xb in U ;

assume that

A12: f . a9 = f . b9 and

A13: a9 <> b9 ; :: thesis: contradiction

consider xa, ya being Real such that

A14: a9 = xa and

A15: f . a9 = ].ya,xa.[ and

A16: ya < xa and

A17: ].ya,xa.[ misses U by A4, A5, A6;

consider c being Rational such that

A18: ya < c and

A19: c < xa by A16, RAT_1:7;

A20: c in f . a9 by A15, A18, A19, XXREAL_1:4;

then A21: c < xb by A9, A12, XXREAL_1:4;

ex x being Element of REAL st

( xa = x & x is_local_minimum_of U ) by A4, A6, A14;

then A22: xa in U ;

yb < c by A9, A12, A20, XXREAL_1:4;

then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A19, A18, A21, A14, A8, A13, XXREAL_0:1, XXREAL_0:2;

then ( xa in f . b9 or xb in f . a9 ) by A15, A9, XXREAL_1:4;

hence contradiction by A15, A17, A9, A10, A11, A22, XBOOLE_0:3; :: thesis: verum

end;set a = f . a9;

set b = f . b9;

assume that

A6: a9 in dom f and

A7: b9 in dom f ; :: thesis: ( not f . a9 = f . b9 or a9 = b9 )

consider xb, yb being Real such that

A8: b9 = xb and

A9: f . b9 = ].yb,xb.[ and

yb < xb and

A10: ].yb,xb.[ misses U by A4, A5, A7;

ex x being Element of REAL st

( xb = x & x is_local_minimum_of U ) by A4, A7, A8;

then A11: xb in U ;

assume that

A12: f . a9 = f . b9 and

A13: a9 <> b9 ; :: thesis: contradiction

consider xa, ya being Real such that

A14: a9 = xa and

A15: f . a9 = ].ya,xa.[ and

A16: ya < xa and

A17: ].ya,xa.[ misses U by A4, A5, A6;

consider c being Rational such that

A18: ya < c and

A19: c < xa by A16, RAT_1:7;

A20: c in f . a9 by A15, A18, A19, XXREAL_1:4;

then A21: c < xb by A9, A12, XXREAL_1:4;

ex x being Element of REAL st

( xa = x & x is_local_minimum_of U ) by A4, A6, A14;

then A22: xa in U ;

yb < c by A9, A12, A20, XXREAL_1:4;

then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A19, A18, A21, A14, A8, A13, XXREAL_0:1, XXREAL_0:2;

then ( xa in f . b9 or xb in f . a9 ) by A15, A9, XXREAL_1:4;

hence contradiction by A15, A17, A9, A10, A11, A22, XBOOLE_0:3; :: thesis: verum

A24: rng f is mutually-disjoint

proof

let a be set ; :: according to TAXONOM2:def 5 :: thesis: for b_{1} being set holds

( not a in rng f or not b_{1} in rng f or a = b_{1} or a misses b_{1} )

let b be set ; :: thesis: ( not a in rng f or not b in rng f or a = b or a misses b )

assume a in rng f ; :: thesis: ( not b in rng f or a = b or a misses b )

then consider a9 being object such that

A25: a9 in dom f and

A26: a = f . a9 by FUNCT_1:def 3;

consider xa, ya being Real such that

A27: a9 = xa and

A28: a = ].ya,xa.[ and

ya < xa and

A29: ].ya,xa.[ misses U by A4, A5, A25, A26;

ex x being Element of REAL st

( xa = x & x is_local_minimum_of U ) by A4, A25, A27;

then A30: xa in U ;

assume b in rng f ; :: thesis: ( a = b or a misses b )

then consider b9 being object such that

A31: b9 in dom f and

A32: b = f . b9 by FUNCT_1:def 3;

consider xb, yb being Real such that

A33: b9 = xb and

A34: b = ].yb,xb.[ and

yb < xb and

A35: ].yb,xb.[ misses U by A4, A5, A31, A32;

assume that

A36: a <> b and

A37: a meets b ; :: thesis: contradiction

consider c being object such that

A38: c in a and

A39: c in b by A37, XBOOLE_0:3;

reconsider c = c as Element of REAL by A28, A38;

A40: c < xa by A28, A38, XXREAL_1:4;

ex x being Element of REAL st

( xb = x & x is_local_minimum_of U ) by A4, A31, A33;

then A41: xb in U ;

A42: c < xb by A34, A39, XXREAL_1:4;

A43: ya < c by A28, A38, XXREAL_1:4;

yb < c by A34, A39, XXREAL_1:4;

then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A40, A43, A42, A26, A32, A27, A33, A36, XXREAL_0:1, XXREAL_0:2;

then ( xa in b or xb in a ) by A28, A34, XXREAL_1:4;

hence contradiction by A28, A29, A34, A35, A41, A30, XBOOLE_0:3; :: thesis: verum

end;( not a in rng f or not b

let b be set ; :: thesis: ( not a in rng f or not b in rng f or a = b or a misses b )

assume a in rng f ; :: thesis: ( not b in rng f or a = b or a misses b )

then consider a9 being object such that

A25: a9 in dom f and

A26: a = f . a9 by FUNCT_1:def 3;

consider xa, ya being Real such that

A27: a9 = xa and

A28: a = ].ya,xa.[ and

ya < xa and

A29: ].ya,xa.[ misses U by A4, A5, A25, A26;

ex x being Element of REAL st

( xa = x & x is_local_minimum_of U ) by A4, A25, A27;

then A30: xa in U ;

assume b in rng f ; :: thesis: ( a = b or a misses b )

then consider b9 being object such that

A31: b9 in dom f and

A32: b = f . b9 by FUNCT_1:def 3;

consider xb, yb being Real such that

A33: b9 = xb and

A34: b = ].yb,xb.[ and

yb < xb and

A35: ].yb,xb.[ misses U by A4, A5, A31, A32;

assume that

A36: a <> b and

A37: a meets b ; :: thesis: contradiction

consider c being object such that

A38: c in a and

A39: c in b by A37, XBOOLE_0:3;

reconsider c = c as Element of REAL by A28, A38;

A40: c < xa by A28, A38, XXREAL_1:4;

ex x being Element of REAL st

( xb = x & x is_local_minimum_of U ) by A4, A31, A33;

then A41: xb in U ;

A42: c < xb by A34, A39, XXREAL_1:4;

A43: ya < c by A28, A38, XXREAL_1:4;

yb < c by A34, A39, XXREAL_1:4;

then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A40, A43, A42, A26, A32, A27, A33, A36, XXREAL_0:1, XXREAL_0:2;

then ( xa in b or xb in a ) by A28, A34, XXREAL_1:4;

hence contradiction by A28, A29, A34, A35, A41, A30, XBOOLE_0:3; :: thesis: verum

now :: thesis: for a being set st a in rng f holds

ex y, x being Real st

( y < x & ].y,x.[ c= a )

then
rng f is countable
by A24, Th18;ex y, x being Real st

( y < x & ].y,x.[ c= a )

let a be set ; :: thesis: ( a in rng f implies ex y, x being Real st

( y < x & ].y,x.[ c= a ) )

assume a in rng f ; :: thesis: ex y, x being Real st

( y < x & ].y,x.[ c= a )

then consider b being object such that

A44: b in dom f and

A45: a = f . b by FUNCT_1:def 3;

consider x, y being Real such that

b = x and

A46: a = ].y,x.[ and

A47: y < x and

].y,x.[ misses U by A4, A5, A44, A45;

take y = y; :: thesis: ex x being Real st

( y < x & ].y,x.[ c= a )

take x = x; :: thesis: ( y < x & ].y,x.[ c= a )

thus ( y < x & ].y,x.[ c= a ) by A46, A47; :: thesis: verum

end;( y < x & ].y,x.[ c= a ) )

assume a in rng f ; :: thesis: ex y, x being Real st

( y < x & ].y,x.[ c= a )

then consider b being object such that

A44: b in dom f and

A45: a = f . b by FUNCT_1:def 3;

consider x, y being Real such that

b = x and

A46: a = ].y,x.[ and

A47: y < x and

].y,x.[ misses U by A4, A5, A44, A45;

take y = y; :: thesis: ex x being Real st

( y < x & ].y,x.[ c= a )

take x = x; :: thesis: ( y < x & ].y,x.[ c= a )

thus ( y < x & ].y,x.[ c= a ) by A46, A47; :: thesis: verum

then card (rng f) c= omega ;

hence card { x where x is Element of REAL : x is_local_minimum_of U } c= omega by A23; :: according to CARD_3:def 14 :: thesis: verum