let T be non empty TopSpace; ( 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 <> {} )
( ( 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
;
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;
( 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
;
meet F <> {}
assume A5:
meet F = {}
;
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
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;
verum
end;
assume A15:
for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {}
; T is countably_compact
let F be Subset-Family of T; COMPL_SP:def 9 ( 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
; 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; ( F9 c= F & F9 is Cover of T & F9 is finite )
thus
F9 c= F
( F9 is Cover of T & F9 is finite )
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; verum