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

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 b₁ being Subset of S ex i being Element of N st b₁ = 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 b₃ being Subset of S holds
( b₃ is Subset of S,N iff ex i being Element of N st b₃ = 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 b₁ being Subset of S,N holds not b₁ 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 b₁ being non empty strict NetStr over L st
( the carrier of b₁ = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b₁ holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b₁ holds b₁ . i = i `1 ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict NetStr over L st the carrier of b₁ = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b₁ holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b₁ holds b₁ . i = i `1 ) & the carrier of b<sub>2</sub> = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b<sub>2</sub> holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b<sub>2</sub> holds b<sub>2</sub> . i = i `1 ) holds
b₁ = b₂

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 b₄ being non empty strict NetStr over L holds
( b₄ = a_net F iff ( the carrier of b₄ = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b₄ holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b₄ holds b₄ . 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 :: 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 ;

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 b₁ being full SubNetStr of N holds b₁ 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 b₁ being SubNetStr of N st
( b₁ is strict & not b₁ is empty & b₁ is directed & b₁ 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;