let T be non empty TopSpace; :: thesis: ( T is compact iff for N being net of T st N is Cauchy holds

N is convergent )

thus ( T is compact implies for N being net of T st N is Cauchy holds

N is convergent ) :: thesis: ( ( for N being net of T st N is Cauchy holds

N is convergent ) implies T is compact )

N is convergent ; :: thesis: T is compact

N is convergent )

thus ( T is compact implies for N being net of T st N is Cauchy holds

N is convergent ) :: thesis: ( ( for N being net of T st N is Cauchy holds

N is convergent ) implies T is compact )

proof

assume A7:
for N being net of T st N is Cauchy holds
assume A1:
T is compact
; :: thesis: for N being net of T st N is Cauchy holds

N is convergent

let N be net of T; :: thesis: ( N is Cauchy implies N is convergent )

assume A2: for A being Subset of T holds

( N is_eventually_in A or N is_eventually_in A ` ) ; :: according to YELLOW19:def 5 :: thesis: N is convergent

consider x being Point of T such that

A3: x is_a_cluster_point_of N by A1, Lm1;

hence N is convergent by YELLOW_6:def 16; :: thesis: verum

end;N is convergent

let N be net of T; :: thesis: ( N is Cauchy implies N is convergent )

assume A2: for A being Subset of T holds

( N is_eventually_in A or N is_eventually_in A ` ) ; :: according to YELLOW19:def 5 :: thesis: N is convergent

consider x being Point of T such that

A3: x is_a_cluster_point_of N by A1, Lm1;

now :: thesis: for V being a_neighborhood of x holds N is_eventually_in V

then
x in Lim N
by YELLOW_6:def 15;let V be a_neighborhood of x; :: thesis: N is_eventually_in V

assume not N is_eventually_in V ; :: thesis: contradiction

then N is_eventually_in V ` by A2;

then consider i being Element of N such that

A4: for j being Element of N st i <= j holds

N . j in V ` ;

N is_often_in V by A3;

then consider j being Element of N such that

A5: i <= j and

A6: N . j in V ;

N . j in V ` by A4, A5;

hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum

end;assume not N is_eventually_in V ; :: thesis: contradiction

then N is_eventually_in V ` by A2;

then consider i being Element of N such that

A4: for j being Element of N st i <= j holds

N . j in V ` ;

N is_often_in V by A3;

then consider j being Element of N such that

A5: i <= j and

A6: N . j in V ;

N . j in V ` by A4, A5;

hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum

hence N is convergent by YELLOW_6:def 16; :: thesis: verum

N is convergent ; :: thesis: T is compact

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

hence
T is compact
by Th31; :: thesis: verumlet F be ultra Filter of (BoolePoset ([#] T)); :: thesis: ex x being Point of T st x is_a_convergence_point_of F,T

set x = the Element of Lim (a_net F);

a_net F is convergent by A7;

then A8: Lim (a_net F) <> {} by YELLOW_6:def 16;

then the Element of Lim (a_net F) in Lim (a_net F) ;

then reconsider x = the Element of Lim (a_net F) 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 by A8, Th17; :: thesis: verum

end;set x = the Element of Lim (a_net F);

a_net F is convergent by A7;

then A8: Lim (a_net F) <> {} by YELLOW_6:def 16;

then the Element of Lim (a_net F) in Lim (a_net F) ;

then reconsider x = the Element of Lim (a_net F) 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 by A8, Th17; :: thesis: verum