let T be non empty TopSpace; :: thesis: ( T is countably_compact iff for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} )
thus ( T is countably_compact implies for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} ) :: thesis: ( ( for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} ) implies T is countably_compact )
proof
assume A1: T is countably_compact ; :: thesis: for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {}
let F be Subset-Family of T; :: thesis: ( F is centered & F is closed & F is countable implies meet F <> {} )
assume that
A2: F is centered and
A3: F is closed and
A4: F is countable ; :: thesis: meet F <> {}
assume A5: meet F = {} ; :: thesis: contradiction
F <> {} by A2, FINSET_1:def 3;
then union (COMPLEMENT F) = (meet F) ` by TOPS_2:7
.= [#] T by A5 ;
then A6: COMPLEMENT F is Cover of T by SETFAM_1:45;
A7: COMPLEMENT F is countable by A4, TOPGEN_4:1;
COMPLEMENT F is open by A3, TOPS_2:9;
then consider G9 being Subset-Family of T such that
A8: G9 c= COMPLEMENT F and
A9: G9 is Cover of T and
A10: G9 is finite by A1, A6, A7;
A11: COMPLEMENT G9 is finite by A10, TOPS_2:8;
A12: COMPLEMENT G9 c= F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT G9 or x in F )
assume A13: x in COMPLEMENT G9 ; :: thesis: x in F
reconsider x9 = x as Subset of T by A13;
x9 ` in G9 by A13, SETFAM_1:def 7;
then (x9 `) ` in F by A8, SETFAM_1:def 7;
hence x in F ; :: thesis: verum
end;
G9 <> {} by A9, TOPS_2:3;
then A14: COMPLEMENT G9 <> {} by TOPS_2:5;
meet (COMPLEMENT G9) = (union G9) ` by A9, TOPS_2:3, TOPS_2:6
.= ([#] T) \ ([#] T) by A9, SETFAM_1:45
.= {} by XBOOLE_1:37 ;
hence contradiction by A2, A12, A14, A11, FINSET_1:def 3; :: thesis: verum
end;
assume A15: for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} ; :: thesis: T is countably_compact
let F be Subset-Family of T; :: according to COMPL_SP:def 9 :: thesis: ( F is Cover of T & F is open & F is countable implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A16: F is Cover of T and
A17: F is open and
A18: F is countable ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
A19: COMPLEMENT F is countable by A18, TOPGEN_4:1;
F <> {} by A16, TOPS_2:3;
then A20: COMPLEMENT F <> {} by TOPS_2:5;
A21: COMPLEMENT F is closed by A17, TOPS_2:10;
meet (COMPLEMENT F) = (union F) ` by A16, TOPS_2:3, TOPS_2:6
.= ([#] T) \ ([#] T) by A16, SETFAM_1:45
.= {} by XBOOLE_1:37 ;
then not COMPLEMENT F is centered by A15, A19, A21;
then consider G9 being set such that
A22: G9 <> {} and
A23: G9 c= COMPLEMENT F and
A24: G9 is finite and
A25: meet G9 = {} by A20, FINSET_1:def 3;
reconsider G9 = G9 as Subset-Family of T by A23, XBOOLE_1:1;
take F9 = COMPLEMENT G9; :: thesis: ( F9 c= F & F9 is Cover of T & F9 is finite )
thus F9 c= F :: thesis: ( F9 is Cover of T & F9 is finite )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F9 or x in F )
assume A26: x in F9 ; :: thesis: x in F
reconsider x9 = x as Subset of T by A26;
x9 ` in G9 by A26, SETFAM_1:def 7;
then (x9 `) ` in F by A23, SETFAM_1:def 7;
hence x in F ; :: thesis: verum
end;
union F9 = (meet G9) ` by A22, TOPS_2:7
.= [#] T by A25 ;
hence ( F9 is Cover of T & F9 is finite ) by A24, SETFAM_1:45, TOPS_2:8; :: thesis: verum