deffunc H1( set ) -> set = { x where x is Element of REAL : x is_local_minimum_of $1 } ;
let A be Subset-Family of REAL; :: thesis: ( card A in continuum implies card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum )
assume A1: card A in continuum ; :: thesis: card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum
A2: now :: thesis: (card A) *` omega in continuum
per cases ( card A is empty or ( not card A is empty & card A is finite ) or card A is infinite ) ;
end;
end;
set Y = { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ;
set X = { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ;
A6: for a being set st a in A holds
H1(a) in bool REAL
proof
let a be set ; :: thesis: ( a in A implies H1(a) in bool REAL )
H1(a) c= REAL
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in H1(a) or b in REAL )
assume b in H1(a) ; :: thesis: b in REAL
then ex x being Element of REAL st
( b = x & x is_local_minimum_of a ) ;
hence b in REAL ; :: thesis: verum
end;
hence ( a in A implies H1(a) in bool REAL ) ; :: thesis: verum
end;
consider f being Function of A,(bool REAL) such that
A7: for a being set st a in A holds
f . a = H1(a) from FUNCT_2:sch 11(A6);
 A8: { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } or a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } )
assume a in { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ; :: thesis: a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) }
then consider x being Element of REAL such that
A9: a = x and
A10: ex U being set st
( U in UniCl A & x is_local_minimum_of U ) ;
consider U being set such that
A11: U in UniCl A and
A12: x is_local_minimum_of U by A10;
reconsider U = U as Subset of REAL by A11;
consider B being Subset-Family of REAL such that
A13: B c= A and
A14: U = union B by A11, CANTOR_1:def 1;
x in U by A12;
then consider C being set such that
A15: x in C and
A16: C in B by A14, TARSKI:def 4;
consider y being Real such that
A17: y < x and
A18: ].y,x.[ misses U by A12;
reconsider C = C as Subset of REAL by A16;
].y,x.[ misses C
proof
assume not ].y,x.[ misses C ; :: thesis: contradiction
then consider b being object such that
A19: b in ].y,x.[ and
A20: b in C by XBOOLE_0:3;
b in U by A14, A16, A20, TARSKI:def 4;
hence contradiction by A18, A19, XBOOLE_0:3; :: thesis: verum
end;
then x is_local_minimum_of C by A17, A15;
hence a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } by A13, A16, A9; :: thesis: verum
end;
{ x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } c= Union f
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } or a in Union f )
A21: dom f = A by FUNCT_2:def 1;
assume a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ; :: thesis: a in Union f
then consider x being Element of REAL such that
A22: a = x and
A23: ex U being set st
( U in A & x is_local_minimum_of U ) ;
consider U being set such that
A24: U in A and
A25: x is_local_minimum_of U by A23;
A26: f . U = H1(U) by A7, A24;
a in H1(U) by A22, A25;
hence a in Union f by A26, A21, A24, CARD_5:2; :: thesis: verum
end;
then { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= Union f by A8;
then A27: card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= card (Union f) by CARD_1:11;
A28: for a being object st a in A holds
card (f . a) c= omega
proof
let a be object ; :: thesis: ( a in A implies card (f . a) c= omega )
assume A29: a in A ; :: thesis: card (f . a) c= omega
then reconsider b = a as Subset of REAL ;
f . a = H1(b) by A7, A29;
then f . a is countable by Th19;
hence card (f . a) c= omega ; :: thesis: verum
end;
dom f = A by FUNCT_2:def 1;
then card (Union f) c= (card A) *` omega by A28, CARD_2:86;
hence card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum by A27, A2, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum