:: On the characterizations of compactness
:: by Grzegorz Bancerek , Noboru Endou and Yuji Sakai
::
:: Received July 29, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

theorem Th1: :: YELLOW19:1
for X being non empty set
for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty
proof end;

definition
let T be non empty TopSpace;
let x be Point of T;
func NeighborhoodSystem x -> Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 1
 { A where A is a_neighborhood of x : verum } ;
coherence
{ A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T))
proof end;
end;

:: deftheorem defines NeighborhoodSystem YELLOW19:def 1 :
for T being non empty TopSpace
for x being Point of T holds NeighborhoodSystem x = { A where A is a_neighborhood of x : verum } ;

theorem Th2: :: YELLOW19:2
for T being non empty TopSpace
for x being Point of T
for A being set holds
( A in NeighborhoodSystem x iff A is a_neighborhood of x )
proof end;

registration
let T be non empty TopSpace;
let x be Point of T;
cluster NeighborhoodSystem x -> non empty proper filtered upper ;
coherence
( not NeighborhoodSystem x is empty & NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
proof end;
end;

theorem Th3: :: YELLOW19:3
for T being non empty TopSpace
for x being Point of T
for F being upper Subset of (BoolePoset ([#] T)) holds
( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )
proof end;

theorem :: YELLOW19:4
for T being non empty TopSpace
for x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;

theorem :: YELLOW19:5
for T being non empty TopSpace
for A being Subset of T holds
( A is open iff for x being Point of T st x in A holds
for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds
A in F )
proof end;

definition
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
mode Subset of S,N -> Subset of S means :Def2: :: YELLOW19:def 2
 ex i being Element of N st it = rng the mapping of (N | i);
existence
ex b1 being Subset of S ex i being Element of N st b1 = rng the mapping of (N | i)
proof end;
end;

:: deftheorem Def2 defines Subset YELLOW19:def 2 :
for S being non empty 1-sorted
for N being non empty NetStr over S
for b3 being Subset of S holds
( b3 is Subset of S,N iff ex i being Element of N st b3 = rng the mapping of (N | i) );

theorem :: YELLOW19:6
for S being non empty 1-sorted
for N being non empty NetStr over S
for i being Element of N holds rng the mapping of (N | i) is Subset of S,N by Def2;

registration
let S be non empty 1-sorted ;
let N be non empty reflexive NetStr over S;
cluster -> non empty for Subset of S,N;
coherence
for b1 being Subset of S,N holds not b1 is empty
proof end;
end;

theorem Th7: :: YELLOW19:7
for S being non empty 1-sorted
for N being net of S
for i being Element of N
for x being set holds
( x in rng the mapping of (N | i) iff ex j being Element of N st
( i <= j & x = N . j ) )
proof end;

theorem Th8: :: YELLOW19:8
for S being non empty 1-sorted
for N being net of S
for A being Subset of S,N holds N is_eventually_in A
proof end;

theorem :: YELLOW19:9
for S being non empty 1-sorted
for N being net of S
for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F
proof end;

definition
let T be non empty 1-sorted ;
let N be non empty NetStr over T;
func a_filter N -> Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 3
 { A where A is Subset of T : N is_eventually_in A } ;
coherence
{ A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T))
proof end;
end;

:: deftheorem defines a_filter YELLOW19:def 3 :
for T being non empty 1-sorted
for N being non empty NetStr over T holds a_filter N = { A where A is Subset of T : N is_eventually_in A } ;

theorem Th10: :: YELLOW19:10
for T being non empty 1-sorted
for N being non empty NetStr over T
for A being set holds
( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )
proof end;

registration
let T be non empty 1-sorted ;
let N be non empty NetStr over T;
cluster a_filter N -> non empty upper ;
coherence
( not a_filter N is empty & a_filter N is upper )
proof end;
end;

registration
let T be non empty 1-sorted ;
let N be net of T;
cluster a_filter N -> proper filtered ;
coherence
( a_filter N is proper & a_filter N is filtered )
proof end;
end;

theorem Th11: :: YELLOW19:11
for T being non empty TopSpace
for N being net of T
for x being Point of T holds
( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )
proof end;

theorem Th12: :: YELLOW19:12
for T being non empty TopSpace
for N being net of T
for x being Point of T holds
( x in Lim N iff x is_a_convergence_point_of a_filter N,T )
proof end;

definition
let L be non empty 1-sorted ;
let O be non empty Subset of L;
let F be Filter of (BoolePoset O);
func a_net F -> non empty strict NetStr over L means :Def4: :: YELLOW19:def 4
( the carrier of it = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it holds it . i = i `1 ) );
existence
ex b1 being non empty strict NetStr over L st
( the carrier of b1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr over L st the carrier of b1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) & the carrier of b2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b2 holds b2 . i = i `1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines a_net YELLOW19:def 4 :
for L being non empty 1-sorted
for O being non empty Subset of L
for F being Filter of (BoolePoset O)
for b4 being non empty strict NetStr over L holds
( b4 = a_net F iff ( the carrier of b4 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b4 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b4 holds b4 . i = i `1 ) ) );

registration
let L be non empty 1-sorted ;
let O be non empty Subset of L;
let F be Filter of (BoolePoset O);
cluster a_net F -> non empty reflexive transitive strict ;
coherence
( a_net F is reflexive & a_net F is transitive )
proof end;
end;

registration
let L be non empty 1-sorted ;
let O be non empty Subset of L;
let F be proper Filter of (BoolePoset O);
cluster a_net F -> non empty strict directed ;
coherence
a_net F is directed
proof end;
end;

theorem Th13: :: YELLOW19:13
for T being non empty 1-sorted
for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F)
proof end;

theorem Th14: :: YELLOW19:14
for T being non empty 1-sorted
for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F)
proof end;

theorem Th15: :: YELLOW19:15
for T being non empty 1-sorted
for F being Filter of (BoolePoset ([#] T))
for A being non empty Subset of T holds
( A in F iff a_net F is_eventually_in A )
proof end;

theorem Th16: :: YELLOW19:16
for T being non empty TopSpace
for F being proper Filter of (BoolePoset ([#] T))
for x being Point of T holds
( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )
proof end;

theorem Th17: :: YELLOW19:17
for T being non empty TopSpace
for F being proper Filter of (BoolePoset ([#] T))
for x being Point of T holds
( x in Lim (a_net F) iff x is_a_convergence_point_of F,T )
proof end;

theorem Th18: :: YELLOW19:18
for T being non empty TopSpace
for x being Point of T
for A being Subset of T st x in Cl A holds
for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
proof end;

theorem Th19: :: YELLOW19:19
for T being non empty 1-sorted
for A being set
for N being net of T st N is_eventually_in A holds
for S being subnet of N holds S is_eventually_in A
proof end;

theorem Th20: :: YELLOW19:20
for T being non empty TopSpace
for F, G, x being set st F c= G & x is_a_convergence_point_of F,T holds
x is_a_convergence_point_of G,T
proof end;

theorem Th21: :: YELLOW19:21
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Cl A iff ex N being net of T st
( N is_eventually_in A & x is_a_cluster_point_of N ) )
proof end;

theorem Th22: :: YELLOW19:22
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Cl A iff ex N being convergent net of T st
( N is_eventually_in A & x in Lim N ) )
proof end;

theorem :: YELLOW19:23
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for N being net of T st N is_eventually_in A holds
for x being Point of T st x is_a_cluster_point_of N holds
x in A )
proof end;

theorem :: YELLOW19:24
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A )
proof end;

theorem Th25: :: YELLOW19:25
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T ) )
proof end;

theorem Th26: :: YELLOW19:26
for T being non empty TopSpace
for A being Subset of T
for x being Point of T holds
( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_convergence_point_of F,T ) )
proof end;

theorem :: YELLOW19:27
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_cluster_point_of F,T holds
x in A )
proof end;

theorem :: YELLOW19:28
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A )
proof end;

theorem Th29: :: YELLOW19:29
for T being non empty TopSpace
for N being net of T
for s being Point of T holds
( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )
proof end;

theorem :: YELLOW19:30
for T being non empty TopSpace
for F being Subset-Family of T st F is closed holds
FinMeetCl F is closed
proof end;

Lm1: for T being non empty TopSpace st T is compact holds
for N being net of T ex x being Point of T st x is_a_cluster_point_of N
proof end;

Lm2: for T being non empty TopSpace st ( for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ) holds
T is compact
proof end;

theorem Th31: :: YELLOW19:31
for T being non empty TopSpace holds
( 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 )
proof end;

theorem :: YELLOW19:32
for T being non empty TopSpace holds
( T is compact iff for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T )
proof end;

theorem Th33: :: YELLOW19:33
for T being non empty TopSpace holds
( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N )
proof end;

theorem :: YELLOW19:34
for T being non empty TopSpace holds
( T is compact iff for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ) by Lm1, Lm2;

registration
let L be non empty 1-sorted ;
let N be transitive NetStr over L;
cluster full -> transitive full for SubNetStr of N;
coherence
for b1 being full SubNetStr of N holds b1 is transitive
proof end;
end;

registration
let L be non empty 1-sorted ;
let N be non empty directed NetStr over L;
cluster non empty strict directed full for SubNetStr of N;
existence
ex b1 being SubNetStr of N st
( b1 is strict & not b1 is empty & b1 is directed & b1 is full )
proof end;
end;

theorem :: YELLOW19:35
for T being non empty TopSpace holds
( T is compact iff for N being net of T ex S being subnet of N st S is convergent )
proof end;

definition
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
attr N is Cauchy means :: YELLOW19:def 5
 for A being Subset of S holds
( N is_eventually_in A or N is_eventually_in A ` );
end;

:: deftheorem defines Cauchy YELLOW19:def 5 :
for S being non empty 1-sorted
for N being non empty NetStr over S holds
( N is Cauchy iff for A being Subset of S holds
( N is_eventually_in A or N is_eventually_in A ` ) );

registration
let S be non empty 1-sorted ;
let F be ultra Filter of (BoolePoset ([#] S));
cluster a_net F -> non empty strict Cauchy ;
coherence
a_net F is Cauchy
proof end;
end;

theorem :: YELLOW19:36
for T being non empty TopSpace holds
( T is compact iff for N being net of T st N is Cauchy holds
N is convergent )
proof end;