let T be non empty TopSpace; :: thesis: for x being Element of (InclPoset the topology of T)
for X being Subset of T st x = X holds
( x is compact iff X is compact )
let x be Element of (InclPoset the topology of T); :: thesis: for X being Subset of T st x = X holds
( x is compact iff X is compact )
let X be Subset of T; :: thesis: ( x = X implies ( x is compact iff X is compact ) )
assume A1: x = X ; :: thesis: ( x is compact iff X is compact )
hereby :: thesis: ( X is compact implies x is compact )
assume x is compact ; :: thesis: X is compact
then A2: x << x ;
thus X is compact :: thesis: verum
proof
let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( not F is Cover of X or not F is open or ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of X & b1 is finite ) )
assume that
A3: X c= union F and
A4: F is open ; :: according to SETFAM_1:def 11 :: thesis: ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of X & b1 is finite )
consider G being finite Subset of F such that
A5: x c= union G by A1, A2, A3, A4, Th34;
reconsider G = G as Subset-Family of T by XBOOLE_1:1;
take G ; :: thesis: ( G c= F & G is Cover of X & G is finite )
thus ( G c= F & X c= union G & G is finite ) by A1, A5; :: according to SETFAM_1:def 11 :: thesis: verum
end;
end;
assume A6: for F being Subset-Family of T st F is Cover of X & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of X & G is finite ) ; :: according to COMPTS_1:def 4 :: thesis: x is compact
now :: thesis: for F being Subset-Family of T st F is open & x c= union F holds
ex G being finite Subset of F st x c= union G
let F be Subset-Family of T; :: thesis: ( F is open & x c= union F implies ex G being finite Subset of F st x c= union G )
assume that
A7: F is open and
A8: x c= union F ; :: thesis: ex G being finite Subset of F st x c= union G
F is Cover of X by A1, A8, SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A9: G c= F and
A10: G is Cover of X and
A11: G is finite by A6, A7;
x c= union G by A1, A10, SETFAM_1:def 11;
hence ex G being finite Subset of F st x c= union G by A9, A11; :: thesis: verum
end;
hence x << x by Th35; :: according to WAYBEL_3:def 2 :: thesis: verum