:: 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
proofend;

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))
proofend;
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 )
proofend;

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 )
proofend;
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 )
proofend;

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 )
proofend;

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)
proofend;
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
proofend;
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 &amp; x = N . j ) )
proofend;

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
proofend;

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
proofend;

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))
proofend;
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 &amp; A is Subset of T ) )
proofend;

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 &amp; a_filter N is upper )
proofend;
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 &amp; a_filter N is filtered )
proofend;
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 )
proofend;

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 )
proofend;

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  }  &amp; ( for i, j being Element of it holds
( i <= j iff j `2 c= i `2 ) ) &amp; ( 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  }  &amp; ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) &amp; ( for i being Element of b1 holds b1 . i = i `1 ) )
proofend;
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  }  &amp; ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) &amp; ( for i being Element of b1 holds b1 . i = i `1 ) &amp; the carrier of b2 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  &amp; ( for i, j being Element of b2 holds
( i <= j iff j `2 c= i `2 ) ) &amp; ( for i being Element of b2 holds b2 . i = i `1 ) holds
b1 = b2
proofend;
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  }  &amp; ( for i, j being Element of b4 holds
( i <= j iff j `2 c= i `2 ) ) &amp; ( 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 &amp; a_net F is transitive )
proofend;
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
proofend;
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)
proofend;

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)
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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

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 &amp; x is_a_cluster_point_of N ) )
proofend;

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 &amp; x in Lim N ) )
proofend;

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 )
proofend;

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 )
proofend;

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 &amp; x is_a_cluster_point_of F,T ) )
proofend;

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 &amp; x is_a_convergence_point_of F,T ) )
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;
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 &amp; not b1 is empty &amp; b1 is directed &amp; b1 is full )
proofend;
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 )
proofend;

definition
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
attrN 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
proofend;
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 )
proofend;