:: YELLOW19 semantic presentation

theorem Th1: :: YELLOW19:1

canceled;

theorem Th2: :: YELLOW19:2

for b₁ being non empty set
for b₂ being proper Filter of (BoolePoset b₁)
for b₃ being set st b₃ in b₂ holds
not b₃ is empty

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
func NeighborhoodSystem c₂ -> Subset of (BoolePoset ([#] a₁)) equals :: YELLOW19:def 1
{ b₁ where B is a_neighborhood of a₂ : verum } ;
coherence

proof end;

end;

:: deftheorem Def1 defines NeighborhoodSystem YELLOW19:def 1 :

theorem Th3: :: YELLOW19:3

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being set holds
( b₃ in NeighborhoodSystem b₂ iff b₃ is a_neighborhood of b₂ )

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster NeighborhoodSystem a₂ -> non empty filtered upper proper ;
coherence

proof end;

end;

theorem Th4: :: YELLOW19:4

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being upper Subset of (BoolePoset ([#] b₁)) holds
( b₂ is_a_convergence_point_of b₃,b₁ iff NeighborhoodSystem b₂ c= b₃ )

proof end;

theorem Th5: :: YELLOW19:5

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ is_a_convergence_point_of NeighborhoodSystem b₂,b₁ by Th4;

theorem Th6: :: YELLOW19:6

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is open iff for b₃ being Point of b₁ st b₃ in b₂ holds
for b₄ being Filter of (BoolePoset ([#] b₁)) st b₃ is_a_convergence_point_of b₄,b₁ holds
b₂ in b₄ )

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
mode Subset of c₁,c₂ -> Subset of a₁ means :Def2: :: YELLOW19:def 2
ex b₁ being Element of a₂ st a₃ = rng the mapping of (a₂ | b₁);
existence

proof end;

end;

:: deftheorem Def2 defines Subset YELLOW19:def 2 :

theorem Th7: :: YELLOW19:7

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₂ holds rng the mapping of (b₂ | b₃) is Subset of b₁,b₂ by Def2;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty reflexive NetStr of c₁;
cluster -> non empty Subset of a₁,a₂;
coherence

proof end;

end;

theorem Th8: :: YELLOW19:8

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being Element of b₂
for b₄ being set holds
( b₄ in rng the mapping of (b₂ | b₃) iff ex b₅ being Element of b₂ st
( b₃ <= b₅ & b₄ = b₂ . b₅ ) )

proof end;

theorem Th9: :: YELLOW19:9

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being Subset of b₁,b₂ holds b₂ is_eventually_in b₃

proof end;

theorem Th10: :: YELLOW19:10

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being non empty finite set st ( for b₄ being Element of b₃ holds b₄ is Subset of b₁,b₂ ) holds
ex b₄ being Subset of b₁,b₂ st b₄ c= meet b₃

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
func a_filter c₂ -> Subset of (BoolePoset ([#] a₁)) equals :: YELLOW19:def 3
{ b₁ where B is Subset of a₁ : a₂ is_eventually_in b₁ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines a_filter YELLOW19:def 3 :

theorem Th11: :: YELLOW19:11

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being set holds
( b₃ in a_filter b₂ iff ( b₂ is_eventually_in b₃ & b₃ is Subset of b₁ ) )

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
cluster a_filter a₂ -> non empty upper ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
cluster a_filter a₂ -> non empty filtered upper proper ;
coherence

proof end;

end;

theorem Th12: :: YELLOW19:12

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ holds
( b₃ is_a_cluster_point_of b₂ iff b₃ is_a_cluster_point_of a_filter b₂,b₁ )

proof end;

theorem Th13: :: YELLOW19:13

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ holds
( b₃ in Lim b₂ iff b₃ is_a_convergence_point_of a_filter b₂,b₁ )

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty Subset of c₁;
let c₃ be Filter of (BoolePoset c₂);
func a_net c₃ -> non empty strict NetStr of a₁ means :Def4: :: YELLOW19:def 4
( the carrier of a₄ = { [b₁,b₂] where B is Element of a₁, B is Element of a₃ : b₁ in b₂ } & ( for b₁, b₂ being Element of a₄ holds
( b₁ <= b₂ iff b₂ `2 c= b₁ `2 ) ) & ( for b₁ being Element of a₄ holds a₄ . b₁ = b₁ `1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines a_net YELLOW19:def 4 :

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty Subset of c₁;
let c₃ be Filter of (BoolePoset c₂);
cluster a_net a₃ -> non empty reflexive transitive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty Subset of c₁;
let c₃ be proper Filter of (BoolePoset c₂);
cluster a_net a₃ -> non empty reflexive transitive strict directed ;
coherence

proof end;

end;

theorem Th14: :: YELLOW19:14

for b₁ being non empty 1-sorted
for b₂ being Filter of (BoolePoset ([#] b₁)) holds b₂ \ {{} } = a_filter (a_net b₂)

proof end;

theorem Th15: :: YELLOW19:15

for b₁ being non empty 1-sorted
for b₂ being proper Filter of (BoolePoset ([#] b₁)) holds b₂ = a_filter (a_net b₂)

proof end;

theorem Th16: :: YELLOW19:16

for b₁ being non empty 1-sorted
for b₂ being Filter of (BoolePoset ([#] b₁))
for b₃ being non empty Subset of b₁ holds
( b₃ in b₂ iff a_net b₂ is_eventually_in b₃ )

proof end;

theorem Th17: :: YELLOW19:17

for b₁ being non empty TopSpace
for b₂ being proper Filter of (BoolePoset ([#] b₁))
for b₃ being Point of b₁ holds
( b₃ is_a_cluster_point_of a_net b₂ iff b₃ is_a_cluster_point_of b₂,b₁ )

proof end;

theorem Th18: :: YELLOW19:18

for b₁ being non empty TopSpace
for b₂ being proper Filter of (BoolePoset ([#] b₁))
for b₃ being Point of b₁ holds
( b₃ in Lim (a_net b₂) iff b₃ is_a_convergence_point_of b₂,b₁ )

proof end;

theorem Th19: :: YELLOW19:19

canceled;

theorem Th20: :: YELLOW19:20

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ st b₂ in Cl b₃ holds
for b₄ being proper Filter of (BoolePoset ([#] b₁)) st b₄ = NeighborhoodSystem b₂ holds
a_net b₄ is_often_in b₃

proof end;

theorem Th21: :: YELLOW19:21

for b₁ being non empty 1-sorted
for b₂ being set
for b₃ being net of b₁ st b₃ is_eventually_in b₂ holds
for b₄ being subnet of b₃ holds b₄ is_eventually_in b₂

proof end;

theorem Th22: :: YELLOW19:22

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being set st b₂ c= b₃ & b₄ is_a_convergence_point_of b₂,b₁ holds
b₄ is_a_convergence_point_of b₃,b₁

proof end;

theorem Th23: :: YELLOW19:23

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff ex b₄ being net of b₁ st
( b₄ is_eventually_in b₂ & b₃ is_a_cluster_point_of b₄ ) )

proof end;

theorem Th24: :: YELLOW19:24

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff ex b₄ being convergent net of b₁ st
( b₄ is_eventually_in b₂ & b₃ in Lim b₄ ) )

proof end;

theorem Th25: :: YELLOW19:25

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is closed iff for b₃ being net of b₁ st b₃ is_eventually_in b₂ holds
for b₄ being Point of b₁ st b₄ is_a_cluster_point_of b₃ holds
b₄ in b₂ )

proof end;

theorem Th26: :: YELLOW19:26

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is closed iff for b₃ being convergent net of b₁ st b₃ is_eventually_in b₂ holds
for b₄ being Point of b₁ st b₄ in Lim b₃ holds
b₄ in b₂ )

proof end;

theorem Th27: :: YELLOW19:27

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff ex b₄ being proper Filter of (BoolePoset ([#] b₁)) st
( b₂ in b₄ & b₃ is_a_cluster_point_of b₄,b₁ ) )

proof end;

theorem Th28: :: YELLOW19:28

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff ex b₄ being ultra Filter of (BoolePoset ([#] b₁)) st
( b₂ in b₄ & b₃ is_a_convergence_point_of b₄,b₁ ) )

proof end;

theorem Th29: :: YELLOW19:29

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is closed iff for b₃ being proper Filter of (BoolePoset ([#] b₁)) st b₂ in b₃ holds
for b₄ being Point of b₁ st b₄ is_a_cluster_point_of b₃,b₁ holds
b₄ in b₂ )

proof end;

theorem Th30: :: YELLOW19:30

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is closed iff for b₃ being ultra Filter of (BoolePoset ([#] b₁)) st b₂ in b₃ holds
for b₄ being Point of b₁ st b₄ is_a_convergence_point_of b₃,b₁ holds
b₄ in b₂ )

proof end;

theorem Th31: :: YELLOW19:31

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ holds
( b₃ is_a_cluster_point_of b₂ iff for b₄ being Subset of b₁,b₂ holds b₃ in Cl b₄ )

proof end;

theorem Th32: :: YELLOW19:32

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st b₂ is closed holds
FinMeetCl b₂ is closed

proof end;

Lemma24: for b₁ being non empty TopSpace st b₁ is compact holds
for b₂ being net of b₁ ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂

proof end;

Lemma25: for b₁ being non empty TopSpace st ( for b₂ being net of b₁ st b₂ in NetUniv b₁ holds
ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ ) holds
b₁ is compact

proof end;

theorem Th33: :: YELLOW19:33

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being ultra Filter of (BoolePoset ([#] b₁)) ex b₃ being Point of b₁ st b₃ is_a_convergence_point_of b₂,b₁ )

proof end;

theorem Th34: :: YELLOW19:34

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being proper Filter of (BoolePoset ([#] b₁)) ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂,b₁ )

proof end;

theorem Th35: :: YELLOW19:35

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being net of b₁ ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ )

proof end;

theorem Th36: :: YELLOW19:36

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being net of b₁ st b₂ in NetUniv b₁ holds
ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ ) by Lemma24, Lemma25;

registration

let c₁ be non empty 1-sorted ;
let c₂ be transitive NetStr of c₁;
cluster full -> transitive full SubNetStr of a₂;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty directed NetStr of c₁;
cluster non empty strict directed full SubNetStr of a₂;
existence

proof end;

end;

theorem Th37: :: YELLOW19:37

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being net of b₁ ex b₃ being subnet of b₂ st b₃ is convergent )

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
attr a₂ is Cauchy means :: YELLOW19:def 5
for b₁ being Subset of a₁ holds
( a₂ is_eventually_in b₁ or a₂ is_eventually_in b₁ ` );

end;

:: deftheorem Def5 defines Cauchy YELLOW19:def 5 :

registration

let c₁ be non empty 1-sorted ;
let c₂ be ultra Filter of (BoolePoset ([#] c₁));
cluster a_net a₂ -> non empty reflexive transitive strict directed Cauchy ;
coherence

proof end;

end;

theorem Th38: :: YELLOW19:38

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being net of b₁ st b₂ is Cauchy holds
b₂ is convergent )

proof end;