:: WAYBEL33 semantic presentation

definition

let c₁ be non empty Poset;
let c₂ be non empty Subset of c₁;
let c₃ be Filter of (BoolePoset c₂);
func lim_inf c₃ -> Element of a₁ equals :: WAYBEL33:def 1
"\/" { (inf b₁) where B is Subset of a₁ : b₁ in a₃ } ,a₁;
correctness ;

end;

:: deftheorem Def1 defines lim_inf WAYBEL33:def 1 :

theorem Th1: :: WAYBEL33:1

for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being Filter of (BoolePoset b₃)
for b₆ being Filter of (BoolePoset b₄) st b₅ = b₆ holds
lim_inf b₅ = lim_inf b₆

proof end;

definition

let c₁ be non empty TopRelStr ;
attr a₁ is lim-inf means :Def2: :: WAYBEL33:def 2
the topology of a₁ = xi a₁;

end;

:: deftheorem Def2 defines lim-inf WAYBEL33:def 2 :

registration

cluster non empty lim-inf -> non empty TopSpace-like TopRelStr ;
coherence

proof end;

end;

registration

cluster trivial -> lim-inf TopRelStr ;
coherence

proof end;

end;

registration

cluster continuous complete lim-inf TopRelStr ;
existence

proof end;

end;

theorem Th2: :: WAYBEL33:2

for b₁, b₂ being non empty 1-sorted st the carrier of b₁ = the carrier of b₂ holds
for b₃ being NetStr of b₁ ex b₄ being strict NetStr of b₂ st
( RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & the mapping of b₃ = the mapping of b₄ )

proof end;

theorem Th3: :: WAYBEL33:3

for b₁, b₂ being non empty 1-sorted st the carrier of b₁ = the carrier of b₂ holds
for b₃ being NetStr of b₁ st b₃ in NetUniv b₁ holds
ex b₄ being strict net of b₂ st
( b₄ in NetUniv b₂ & RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & the mapping of b₃ = the mapping of b₄ )

proof end;

E4: now

let c₁, c₂ be non empty RelStr ;
let c₃ be net of c₁;
let c₄ be net of c₂;
assume E5: ( RelStr(# the carrier of c₃,the InternalRel of c₃ #) = RelStr(# the carrier of c₄,the InternalRel of c₄ #) & the mapping of c₃ = the mapping of c₄ ) ;
deffunc H₁( Element of c₃) -> set = { (c₃ . b₁) where B is Element of c₃ : b₁ >= a₁ } ;
deffunc H₂( Element of c₄) -> set = { (c₄ . b₁) where B is Element of c₄ : b₁ >= a₁ } ;
let c₅ be Element of c₃;
let c₆ be Element of c₄;
assume E6: c₅ = c₆ ;
thus H₁(c₅) c= H₂(c₆)

proof

let c₇ be set ; :: according to TARSKI:def 3
assume c₇ in H₁(c₅) ;
then consider c₈ being Element of c₃ such that
E7: ( c₇ = c₃ . c₈ & c₈ >= c₅ ) ;
reconsider c₉ = c₈, c₁₀ = c₅ as Element of c₃ ;
reconsider c₁₁ = c₉, c₁₂ = c₆ as Element of c₄ by E5;
E8: c₁₁ >= c₁₂ by E5, E6, E7, YELLOW_0:1;
c₃ . c₉ = the mapping of c₃ . c₉
.= c₄ . c₁₁ by E5 ;
hence c₇ in H₂(c₆) by E7, E8;

end;

E5: now

let c₁, c₂ be /\-complete Semilattice;
assume E6: RelStr(# the carrier of c₁,the InternalRel of c₁ #) = RelStr(# the carrier of c₂,the InternalRel of c₂ #) ;
let c₃ be net of c₁;
let c₄ be net of c₂;
assume E7: ( RelStr(# the carrier of c₃,the InternalRel of c₃ #) = RelStr(# the carrier of c₄,the InternalRel of c₄ #) & the mapping of c₃ = the mapping of c₄ ) ;
deffunc H₁( Element of c₃) -> set = { (c₃ . b₁) where B is Element of c₃ : b₁ >= a₁ } ;
deffunc H₂( Element of c₄) -> set = { (c₄ . b₁) where B is Element of c₄ : b₁ >= a₁ } ;
set c₅ = { ("/\" H₁(b₁),c₁) where B is Element of c₃ : verum } ;
set c₆ = { ("/\" H₂(b₁),c₂) where B is Element of c₄ : verum } ;
thus { ("/\" H₁(b₁),c₁) where B is Element of c₃ : verum } c= { ("/\" H₂(b₁),c₂) where B is Element of c₄ : verum }

proof

let c₇ be set ; :: according to TARSKI:def 3
assume c₇ in { ("/\" H₁(b₁),c₁) where B is Element of c₃ : verum } ;
then consider c₈ being Element of c₃ such that
E8: c₇ = "/\" H₁(c₈),c₁ ;
reconsider c₉ = c₈ as Element of c₄ by E7;
E9: H₁(c₈) = H₂(c₉)

proof

thus ( H₁(c₈) c= H₂(c₉) & H₂(c₉) c= H₁(c₈) ) by E7, Lemma4; :: according to XBOOLE_0:def 10

end;

reconsider c₁₀ = c₈ as Element of c₃ ;
( [#] c₃ = the carrier of c₃ & [#] c₃ is directed ) by WAYBEL_0:def 6;
then consider c₁₁ being Element of c₃ such that
c₁₁ in the carrier of c₃ and
E10: ( c₁₀ <= c₁₁ & c₁₀ <= c₁₁ ) by WAYBEL_0:def 1;
E11: c₃ . c₁₁ in H₁(c₁₀) by E10;
H₁(c₁₀) c= the carrier of c₁

proof

let c₁₂ be set ; :: according to TARSKI:def 3
assume c₁₂ in H₁(c₁₀) ;
then ex b₁ being Element of c₃ st
( c₁₂ = c₃ . b₁ & b₁ >= c₁₀ ) ;
hence c₁₂ in the carrier of c₁ ;

end;

then reconsider c₁₂ = H₁(c₁₀) as non empty Subset of c₁ by E11;
ex_inf_of c₁₂,c₁ by WAYBEL_0:76;
then c₇ = "/\" H₂(c₉),c₂ by E6, E8, E9, YELLOW_0:27;
hence c₇ in { ("/\" H₂(b₁),c₂) where B is Element of c₄ : verum } ;

end;

theorem Th4: :: WAYBEL33:4

for b₁, b₂ being up-complete /\-complete Semilattice st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being net of b₁
for b₄ being net of b₂ st RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & the mapping of b₃ = the mapping of b₄ holds
lim_inf b₃ = lim_inf b₄

proof end;

theorem Th5: :: WAYBEL33:5

for b₁, b₂ being non empty 1-sorted st the carrier of b₁ = the carrier of b₂ holds
for b₃ being net of b₁
for b₄ being net of b₂ st RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & the mapping of b₃ = the mapping of b₄ holds
for b₅ being subnet of b₃ ex b₆ being strict subnet of b₄ st
( RelStr(# the carrier of b₅,the InternalRel of b₅ #) = RelStr(# the carrier of b₆,the InternalRel of b₆ #) & the mapping of b₅ = the mapping of b₆ )

proof end;

theorem Th6: :: WAYBEL33:6

for b₁, b₂ being up-complete /\-complete Semilattice st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being NetStr of b₁
for b₄ being set st [b₃,b₄] in lim_inf-Convergence b₁ holds
ex b₅ being strict net of b₂ st
( [b₅,b₄] in lim_inf-Convergence b₂ & RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₅,the InternalRel of b₅ #) & the mapping of b₃ = the mapping of b₅ )

proof end;

theorem Th7: :: WAYBEL33:7

for b₁, b₂ being non empty 1-sorted
for b₃ being non empty NetStr of b₁
for b₄ being non empty NetStr of b₂ st RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & the mapping of b₃ = the mapping of b₄ holds
for b₅ being set st b₃ is_eventually_in b₅ holds
b₄ is_eventually_in b₅

proof end;

Lemma10: for b₁, b₂ being up-complete /\-complete Semilattice st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
the topology of (ConvergenceSpace (lim_inf-Convergence b₁)) c= the topology of (ConvergenceSpace (lim_inf-Convergence b₂))

proof end;

theorem Th8: :: WAYBEL33:8

for b₁, b₂ being up-complete /\-complete Semilattice st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
ConvergenceSpace (lim_inf-Convergence b₁) = ConvergenceSpace (lim_inf-Convergence b₂)

proof end;

theorem Th9: :: WAYBEL33:9

for b₁, b₂ being up-complete /\-complete Semilattice st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
xi b₁ = xi b₂

proof end;

registration

let c₁ be non empty reflexive /\-complete RelStr ;
cluster -> /\-complete TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be Semilattice;
cluster -> with_infima TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be up-complete /\-complete Semilattice;
cluster TopSpace-like /\-complete with_infima strict lim-inf TopAugmentation of a₁;
existence

proof end;

end;

theorem Th10: :: WAYBEL33:10

for b₁ being up-complete /\-complete Semilattice
for b₂ being lim-inf TopAugmentation of b₁ holds xi b₁ = the topology of b₂

proof end;

definition

let c₁ be up-complete /\-complete Semilattice;
func Xi c₁ -> strict TopAugmentation of a₁ means :Def3: :: WAYBEL33:def 3
a₂ is lim-inf;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines Xi WAYBEL33:def 3 :

registration

let c₁ be up-complete /\-complete Semilattice;
cluster Xi a₁ -> TopSpace-like /\-complete with_infima strict lim-inf ;
coherence by Def3;

end;

theorem Th11: :: WAYBEL33:11

for b₁ being complete LATTICE
for b₂ being net of b₁ holds lim_inf b₂ = "\/" { (inf (b₂ | b₃)) where B is Element of b₂ : verum } ,b₁

proof end;

theorem Th12: :: WAYBEL33:12

for b₁ being complete LATTICE
for b₂ being proper Filter of (BoolePoset ([#] b₁))
for b₃ being Subset of b₁ st b₃ in b₂ holds
for b₄ being Element of (a_net b₂) st b₄ `2 = b₃ holds
inf b₃ = inf ((a_net b₂) | b₄)

proof end;

theorem Th13: :: WAYBEL33:13

for b₁ being complete LATTICE
for b₂ being proper Filter of (BoolePoset ([#] b₁)) holds lim_inf b₂ = lim_inf (a_net b₂)

proof end;

Lemma17: for b₁ being LATTICE
for b₂ being non empty Subset of (BoolePoset ([#] b₁)) holds { [b₃,b₄] where B is Element of b₁, B is Element of b₂ : b₃ in b₄ } c= [:the carrier of b₁,(bool the carrier of b₁):]

proof end;

theorem Th14: :: WAYBEL33:14

for b₁ being complete LATTICE
for b₂ being proper Filter of (BoolePoset ([#] b₁)) holds a_net b₂ in NetUniv b₁

proof end;

theorem Th15: :: WAYBEL33:15

for b₁ being complete LATTICE
for b₂ being ultra Filter of (BoolePoset ([#] b₁))
for b₃ being greater_or_equal_to_id Function of (a_net b₂),(a_net b₂) holds lim_inf b₂ >= inf ((a_net b₂) * b₃)

proof end;

theorem Th16: :: WAYBEL33:16

for b₁ being complete LATTICE
for b₂ being ultra Filter of (BoolePoset ([#] b₁))
for b₃ being subnet of a_net b₂ holds lim_inf b₂ = lim_inf b₃

proof end;

theorem Th17: :: WAYBEL33:17

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being set st b₂ is_often_in b₃ holds
ex b₄ being strict subnet of b₂ st
( rng the mapping of b₄ c= b₃ & b₄ is SubNetStr of b₂ )

proof end;

theorem Th18: :: WAYBEL33:18

for b₁ being complete lim-inf TopLattice
for b₂ being non empty Subset of b₁ holds
( b₂ is closed iff for b₃ being ultra Filter of (BoolePoset ([#] b₁)) st b₂ in b₃ holds
lim_inf b₃ in b₂ )

proof end;

theorem Th19: :: WAYBEL33:19

for b₁ being non empty reflexive RelStr holds sigma b₁ c= xi b₁

proof end;

theorem Th20: :: WAYBEL33:20

for b₁, b₂ being non empty TopSpace
for b₃ being prebasis of b₁ st b₃ c= the topology of b₂ & the carrier of b₁ in the topology of b₂ holds
the topology of b₁ c= the topology of b₂

proof end;

theorem Th21: :: WAYBEL33:21

for b₁ being complete LATTICE holds omega b₁ c= xi b₁

proof end;

theorem Th22: :: WAYBEL33:22

for b₁, b₂ being TopSpace
for b₃ being non empty TopSpace st b₃ is TopExtension of b₁ & b₃ is TopExtension of b₂ holds
for b₄ being Refinement of b₁,b₂ holds b₃ is TopExtension of b₄

proof end;

theorem Th23: :: WAYBEL33:23

for b₁ being TopSpace
for b₂ being TopExtension of b₁
for b₃ being Subset of b₁ holds
( ( b₃ is open implies b₃ is open Subset of b₂ ) & ( b₃ is closed implies b₃ is closed Subset of b₂ ) )

proof end;

theorem Th24: :: WAYBEL33:24

for b₁ being complete LATTICE holds lambda b₁ c= xi b₁

proof end;

theorem Th25: :: WAYBEL33:25

for b₁ being complete LATTICE
for b₂ being lim-inf TopAugmentation of b₁
for b₃ being correct Lawson TopAugmentation of b₁ holds b₂ is TopExtension of b₃

proof end;

theorem Th26: :: WAYBEL33:26

for b₁ being complete lim-inf TopLattice
for b₂ being ultra Filter of (BoolePoset ([#] b₁)) holds lim_inf b₂ is_a_convergence_point_of b₂,b₁

proof end;

theorem Th27: :: WAYBEL33:27

for b₁ being complete lim-inf TopLattice holds
( b₁ is compact & b₁ is being_T1 )

proof end;