let T be non empty TopSpace; :: thesis: ( T is compact iff for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T )

set X = the carrier of T;

set X = the carrier of T;

hereby :: thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ) implies T is compact )

assume A13:
for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T
; :: thesis: T is compact assume A1:
T is compact
; :: thesis: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T

let F be ultra Filter of (BoolePoset ([#] T)); :: thesis: ex x being Point of T st x is_a_convergence_point_of F,T

set G = { (Cl A) where A is Subset of T : A in F } ;

{ (Cl A) where A is Subset of T : A in F } c= bool the carrier of T

A2: G is centered

G is closed

then the Element of meet G in meet G ;

then reconsider x = the Element of meet G as Point of T ;

take x = x; :: thesis: x is_a_convergence_point_of F,T

thus x is_a_convergence_point_of F,T :: thesis: verum

end;let F be ultra Filter of (BoolePoset ([#] T)); :: thesis: ex x being Point of T st x is_a_convergence_point_of F,T

set G = { (Cl A) where A is Subset of T : A in F } ;

{ (Cl A) where A is Subset of T : A in F } c= bool the carrier of T

proof

then reconsider G = { (Cl A) where A is Subset of T : A in F } as Subset-Family of T ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Cl A) where A is Subset of T : A in F } or x in bool the carrier of T )

assume x in { (Cl A) where A is Subset of T : A in F } ; :: thesis: x in bool the carrier of T

then ex A being Subset of T st

( x = Cl A & A in F ) ;

hence x in bool the carrier of T ; :: thesis: verum

end;assume x in { (Cl A) where A is Subset of T : A in F } ; :: thesis: x in bool the carrier of T

then ex A being Subset of T st

( x = Cl A & A in F ) ;

hence x in bool the carrier of T ; :: thesis: verum

A2: G is centered

proof

set x = the Element of meet G;
set A0 = the Element of F;

reconsider A0 = the Element of F as Subset of T by WAYBEL_7:2;

Cl A0 in G ;

hence G <> {} ; :: according to FINSET_1:def 3 :: thesis: for b_{1} being set holds

( b_{1} = {} or not b_{1} c= G or not b_{1} is finite or not meet b_{1} = {} )

let H be set ; :: thesis: ( H = {} or not H c= G or not H is finite or not meet H = {} )

assume that

A3: H <> {} and

A4: H c= G and

A5: H is finite ; :: thesis: not meet H = {}

reconsider H1 = H as finite Subset-Family of the carrier of T by A4, A5, XBOOLE_1:1;

H1 c= F

then Intersect H1 <> {} by Th1;

hence not meet H = {} by A3, SETFAM_1:def 9; :: thesis: verum

end;reconsider A0 = the Element of F as Subset of T by WAYBEL_7:2;

Cl A0 in G ;

hence G <> {} ; :: according to FINSET_1:def 3 :: thesis: for b

( b

let H be set ; :: thesis: ( H = {} or not H c= G or not H is finite or not meet H = {} )

assume that

A3: H <> {} and

A4: H c= G and

A5: H is finite ; :: thesis: not meet H = {}

reconsider H1 = H as finite Subset-Family of the carrier of T by A4, A5, XBOOLE_1:1;

H1 c= F

proof

then
Intersect H1 in F
by WAYBEL_7:11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1 or x in F )

assume x in H1 ; :: thesis: x in F

then x in G by A4;

then consider A being Subset of T such that

A6: x = Cl A and

A7: A in F ;

A c= Cl A by PRE_TOPC:18;

hence x in F by A6, A7, WAYBEL_7:7; :: thesis: verum

end;assume x in H1 ; :: thesis: x in F

then x in G by A4;

then consider A being Subset of T such that

A6: x = Cl A and

A7: A in F ;

A c= Cl A by PRE_TOPC:18;

hence x in F by A6, A7, WAYBEL_7:7; :: thesis: verum

then Intersect H1 <> {} by Th1;

hence not meet H = {} by A3, SETFAM_1:def 9; :: thesis: verum

G is closed

proof

then A8:
meet G <> {}
by A1, A2, COMPTS_1:4;
let A be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not A in G or A is closed )

assume A in G ; :: thesis: A is closed

then ex B being Subset of T st

( A = Cl B & B in F ) ;

hence A is closed ; :: thesis: verum

end;assume A in G ; :: thesis: A is closed

then ex B being Subset of T st

( A = Cl B & B in F ) ;

hence A is closed ; :: thesis: verum

then the Element of meet G in meet G ;

then reconsider x = the Element of meet G as Point of T ;

take x = x; :: thesis: x is_a_convergence_point_of F,T

thus x is_a_convergence_point_of F,T :: thesis: verum

proof

let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not x in A or A in F )

assume that

A9: A is open and

A10: x in A ; :: thesis: A in F

set B = A ` ;

hence A in F by A11, WAYBEL_7:21; :: thesis: verum

end;assume that

A9: A is open and

A10: x in A ; :: thesis: A in F

set B = A ` ;

A11: now :: thesis: not A ` in F

F is prime
by WAYBEL_7:22;assume
A ` in F
; :: thesis: contradiction

then Cl (A `) in G ;

then A12: A ` in G by A9, PRE_TOPC:22;

not x in A ` by A10, XBOOLE_0:def 5;

hence contradiction by A8, A12, SETFAM_1:def 1; :: thesis: verum

end;then Cl (A `) in G ;

then A12: A ` in G by A9, PRE_TOPC:22;

not x in A ` by A10, XBOOLE_0:def 5;

hence contradiction by A8, A12, SETFAM_1:def 1; :: thesis: verum

hence A in F by A11, WAYBEL_7:21; :: thesis: verum

now :: thesis: for F being Subset-Family of T st F is centered & F is closed holds

meet F <> {}

hence
T is compact
by COMPTS_1:4; :: thesis: verummeet F <> {}

set L = BoolePoset the carrier of T;

let F be Subset-Family of T; :: thesis: ( F is centered & F is closed implies meet F <> {} )

assume A14: ( F is centered & F is closed ) ; :: thesis: meet F <> {}

reconsider Y = F as Subset of (BoolePoset the carrier of T) by WAYBEL_7:2;

set G = uparrow (fininfs Y);

then consider UF being Filter of (BoolePoset the carrier of T) such that

A21: uparrow (fininfs Y) c= UF and

A22: UF is ultra by WAYBEL_7:26;

consider x being Point of T such that

A23: x is_a_convergence_point_of UF,T by A13, A22;

F c= uparrow (fininfs Y) by WAYBEL_0:62;

then A24: F c= UF by A21;

hence meet F <> {} by A25, SETFAM_1:def 1; :: thesis: verum

end;let F be Subset-Family of T; :: thesis: ( F is centered & F is closed implies meet F <> {} )

assume A14: ( F is centered & F is closed ) ; :: thesis: meet F <> {}

reconsider Y = F as Subset of (BoolePoset the carrier of T) by WAYBEL_7:2;

set G = uparrow (fininfs Y);

now :: thesis: not Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y)

then
uparrow (fininfs Y) is proper
;assume
Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y)
; :: thesis: contradiction

then consider x being Element of (BoolePoset the carrier of T) such that

A15: x <= Bottom (BoolePoset the carrier of T) and

A16: x in fininfs Y by WAYBEL_0:def 16;

A17: Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;

consider Z being finite Subset of Y such that

A18: x = "/\" (Z,(BoolePoset the carrier of T)) and

ex_inf_of Z, BoolePoset the carrier of T by A16;

reconsider Z = Z as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;

A19: x = Bottom (BoolePoset the carrier of T) by A15, YELLOW_5:19;

then x <> Top (BoolePoset the carrier of T) by WAYBEL_7:3;

then A20: Z <> {} by A18, YELLOW_0:def 12;

then meet Z <> {} by A14;

hence contradiction by A17, A18, A19, A20, YELLOW_1:20; :: thesis: verum

end;then consider x being Element of (BoolePoset the carrier of T) such that

A15: x <= Bottom (BoolePoset the carrier of T) and

A16: x in fininfs Y by WAYBEL_0:def 16;

A17: Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;

consider Z being finite Subset of Y such that

A18: x = "/\" (Z,(BoolePoset the carrier of T)) and

ex_inf_of Z, BoolePoset the carrier of T by A16;

reconsider Z = Z as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;

A19: x = Bottom (BoolePoset the carrier of T) by A15, YELLOW_5:19;

then x <> Top (BoolePoset the carrier of T) by WAYBEL_7:3;

then A20: Z <> {} by A18, YELLOW_0:def 12;

then meet Z <> {} by A14;

hence contradiction by A17, A18, A19, A20, YELLOW_1:20; :: thesis: verum

then consider UF being Filter of (BoolePoset the carrier of T) such that

A21: uparrow (fininfs Y) c= UF and

A22: UF is ultra by WAYBEL_7:26;

consider x being Point of T such that

A23: x is_a_convergence_point_of UF,T by A13, A22;

F c= uparrow (fininfs Y) by WAYBEL_0:62;

then A24: F c= UF by A21;

A25: now :: thesis: for A being set st A in F holds

x in A

F <> {}
by A14;x in A

let A be set ; :: thesis: ( A in F implies x in A )

assume A26: A in F ; :: thesis: x in A

then reconsider B = A as Subset of T ;

then Cl B = B by PRE_TOPC:22;

hence x in A by A27, PRE_TOPC:24; :: thesis: verum

end;assume A26: A in F ; :: thesis: x in A

then reconsider B = A as Subset of T ;

A27: now :: thesis: for C being Subset of T st C is open & x in C holds

A meets C

B is closed
by A14, A26;A meets C

let C be Subset of T; :: thesis: ( C is open & x in C implies A meets C )

assume that

A28: C is open and

A29: x in C ; :: thesis: A meets C

A30: C in UF by A23, A28, A29;

A in UF by A24, A26;

then reconsider c = C, a = A as Element of (BoolePoset the carrier of T) by A30;

a "/\" c in UF by A24, A26, A30, WAYBEL_0:41;

then a "/\" c <> {} by A22, Th1;

then A /\ C <> {} by YELLOW_1:17;

hence A meets C ; :: thesis: verum

end;assume that

A28: C is open and

A29: x in C ; :: thesis: A meets C

A30: C in UF by A23, A28, A29;

A in UF by A24, A26;

then reconsider c = C, a = A as Element of (BoolePoset the carrier of T) by A30;

a "/\" c in UF by A24, A26, A30, WAYBEL_0:41;

then a "/\" c <> {} by A22, Th1;

then A /\ C <> {} by YELLOW_1:17;

hence A meets C ; :: thesis: verum

then Cl B = B by PRE_TOPC:22;

hence x in A by A27, PRE_TOPC:24; :: thesis: verum

hence meet F <> {} by A25, SETFAM_1:def 1; :: thesis: verum