:: WAYBEL21 semantic presentation

definition

let c₁, c₂ be Semilattice;
assume E1: ( c₁ is upper-bounded implies c₂ is upper-bounded ) ;
mode SemilatticeHomomorphism of c₁,c₂ -> Function of a₁,a₂ means :Def1: :: WAYBEL21:def 1
for b₁ being finite Subset of a₁ holds a₃ preserves_inf_of b₁;
existence

proof end;

end;

:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def 1 :

registration

let c₁, c₂ be Semilattice;
cluster meet-preserving -> monotone M4(the carrier of a₁,the carrier of a₂);
coherence

proof end;

end;

registration

let c₁ be Semilattice;
let c₂ be upper-bounded Semilattice;
cluster -> meet-preserving SemilatticeHomomorphism of a₁,a₂;
coherence

proof end;

end;

theorem Th1: :: WAYBEL21:1

for b₁, b₂ being upper-bounded Semilattice
for b₃ being SemilatticeHomomorphism of b₁,b₂ holds b₃ . (Top b₁) = Top b₂

proof end;

theorem Th2: :: WAYBEL21:2

for b₁, b₂ being Semilattice
for b₃ being Function of b₁,b₂ st b₃ is meet-preserving holds
for b₄ being non empty finite Subset of b₁ holds b₃ preserves_inf_of b₄

proof end;

theorem Th3: :: WAYBEL21:3

for b₁, b₂ being upper-bounded Semilattice
for b₃ being meet-preserving Function of b₁,b₂ st b₃ . (Top b₁) = Top b₂ holds
b₃ is SemilatticeHomomorphism of b₁,b₂

proof end;

theorem Th4: :: WAYBEL21:4

for b₁, b₂ being Semilattice
for b₃ being Function of b₁,b₂ st b₃ is meet-preserving & ( for b₄ being non empty filtered Subset of b₁ holds b₃ preserves_inf_of b₄ ) holds
for b₄ being non empty Subset of b₁ holds b₃ preserves_inf_of b₄

proof end;

theorem Th5: :: WAYBEL21:5

for b₁, b₂ being Semilattice
for b₃ being Function of b₁,b₂ st b₃ is infs-preserving holds
b₃ is SemilatticeHomomorphism of b₁,b₂

proof end;

theorem Th6: :: WAYBEL21:6

for b₁, b₂, b₃, b₄ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) & RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) holds
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st b₅ = b₆ holds
( ( b₅ is infs-preserving implies b₆ is infs-preserving ) & ( b₅ is directed-sups-preserving implies b₆ is directed-sups-preserving ) )

proof end;

theorem Th7: :: WAYBEL21:7

for b₁, b₂, b₃, b₄ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) & RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) holds
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st b₅ = b₆ holds
( ( b₅ is sups-preserving implies b₆ is sups-preserving ) & ( b₅ is filtered-infs-preserving implies b₆ is filtered-infs-preserving ) )

proof end;

theorem Th8: :: WAYBEL21:8

for b₁ being complete LATTICE
for b₂ being non empty full infs-inheriting SubRelStr of b₁ holds incl b₂,b₁ is infs-preserving

proof end;

theorem Th9: :: WAYBEL21:9

for b₁ being complete LATTICE
for b₂ being non empty full sups-inheriting SubRelStr of b₁ holds incl b₂,b₁ is sups-preserving

proof end;

theorem Th10: :: WAYBEL21:10

for b₁ being non empty up-complete Poset
for b₂ being non empty full directed-sups-inheriting SubRelStr of b₁ holds incl b₂,b₁ is directed-sups-preserving

proof end;

theorem Th11: :: WAYBEL21:11

for b₁ being complete LATTICE
for b₂ being non empty full filtered-infs-inheriting SubRelStr of b₁ holds incl b₂,b₁ is filtered-infs-preserving

proof end;

theorem Th12: :: WAYBEL21:12

for b₁, b₂, b₃ being RelStr
for b₄ being SubRelStr of b₁ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & RelStr(# the carrier of b₄,the InternalRel of b₄ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) holds
( b₃ is SubRelStr of b₂ & ( b₄ is full implies b₃ is full SubRelStr of b₂ ) )

proof end;

theorem Th13: :: WAYBEL21:13

for b₁ being non empty RelStr holds b₁ is full infs-inheriting sups-inheriting SubRelStr of b₁

proof end;

registration

let c₁ be complete LATTICE;
cluster complete SubRelStr of a₁;
existence

proof end;

end;

theorem Th14: :: WAYBEL21:14

for b₁ being Semilattice
for b₂ being non empty full SubRelStr of b₁ holds
( b₂ is meet-inheriting iff for b₃ being non empty finite Subset of b₂ holds "/\" b₃,b₁ in the carrier of b₂ )

proof end;

theorem Th15: :: WAYBEL21:15

for b₁ being sup-Semilattice
for b₂ being non empty full SubRelStr of b₁ holds
( b₂ is join-inheriting iff for b₃ being non empty finite Subset of b₂ holds "\/" b₃,b₁ in the carrier of b₂ )

proof end;

theorem Th16: :: WAYBEL21:16

for b₁ being upper-bounded Semilattice
for b₂ being non empty full meet-inheriting SubRelStr of b₁ st Top b₁ in the carrier of b₂ & b₂ is filtered-infs-inheriting holds
b₂ is infs-inheriting

proof end;

theorem Th17: :: WAYBEL21:17

for b₁ being lower-bounded sup-Semilattice
for b₂ being non empty full join-inheriting SubRelStr of b₁ st Bottom b₁ in the carrier of b₂ & b₂ is directed-sups-inheriting holds
b₂ is sups-inheriting

proof end;

theorem Th18: :: WAYBEL21:18

for b₁ being complete LATTICE
for b₂ being non empty full SubRelStr of b₁ st b₂ is infs-inheriting holds
b₂ is complete

proof end;

theorem Th19: :: WAYBEL21:19

for b₁ being complete LATTICE
for b₂ being non empty full SubRelStr of b₁ st b₂ is sups-inheriting holds
b₂ is complete

proof end;

theorem Th20: :: WAYBEL21:20

for b₁, b₂ being non empty RelStr
for b₃ being non empty full SubRelStr of b₁
for b₄ being non empty full SubRelStr of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & the carrier of b₃ = the carrier of b₄ & b₃ is infs-inheriting holds
b₄ is infs-inheriting

proof end;

theorem Th21: :: WAYBEL21:21

proof end;

theorem Th22: :: WAYBEL21:22

proof end;

theorem Th23: :: WAYBEL21:23

proof end;

theorem Th24: :: WAYBEL21:24

for b₁, b₂ being non empty TopSpace
for b₃ being net of b₁
for b₄ being Function of b₁,b₂ st b₄ is continuous holds
b₄ .: (Lim b₃) c= Lim (b₄ * b₃)

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be non empty NetStr of c₁;
redefine attr a₂ is antitone means :Def2: :: WAYBEL21:def 2
for b₁, b₂ being Element of a₂ st b₁ <= b₂ holds
a₂ . b₁ >= a₂ . b₂;
compatibility

proof end;

end;

:: deftheorem Def2 defines antitone WAYBEL21:def 2 :

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be Element of c₁;
cluster {a₂} opp+id -> transitive directed monotone antitone ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster reflexive strict monotone antitone NetStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty Subset of c₁;
cluster a₂ opp+id -> antitone ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty reflexive RelStr ;
let c₃ be monotone Function of c₁,c₂;
let c₄ be non empty antitone NetStr of c₁;
cluster a₃ * a₄ -> antitone ;
coherence

proof end;

end;

theorem Th25: :: WAYBEL21:25

for b₁ being complete LATTICE
for b₂ being net of b₁ holds { ("/\" { (b₂ . b₄) where B is Element of b₂ : b₄ >= b₃ } ,b₁) where B is Element of b₂ : verum } is non empty directed Subset of b₁

proof end;

theorem Th26: :: WAYBEL21:26

for b₁ being non empty Poset
for b₂ being reflexive monotone net of b₁ holds { ("/\" { (b₂ . b₄) where B is Element of b₂ : b₄ >= b₃ } ,b₁) where B is Element of b₂ : verum } is non empty directed Subset of b₁

proof end;

theorem Th27: :: WAYBEL21:27

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being set st rng the mapping of b₂ c= b₃ holds
b₂ is_eventually_in b₃

proof end;

theorem Th28: :: WAYBEL21:28

for b₁ being non empty /\-complete Poset
for b₂ being non empty filtered Subset of b₁ holds lim_inf (b₂ opp+id ) = inf b₂

proof end;

theorem Th29: :: WAYBEL21:29

for b₁, b₂ being non empty /\-complete Poset
for b₃ being non empty filtered Subset of b₁
for b₄ being monotone Function of b₁,b₂ holds lim_inf (b₄ * (b₃ opp+id )) = inf (b₄ .: b₃)

proof end;

theorem Th30: :: WAYBEL21:30

for b₁, b₂ being non empty TopPoset
for b₃ being non empty filtered Subset of b₁
for b₄ being monotone Function of b₁,b₂
for b₅ being non empty filtered Subset of b₂ st b₅ = b₄ .: b₃ holds
b₄ * (b₃ opp+id ) is subnet of b₅ opp+id

proof end;

theorem Th31: :: WAYBEL21:31

proof end;

theorem Th32: :: WAYBEL21:32

for b₁ being non empty reflexive RelStr
for b₂ being non empty Subset of b₁ holds
( the mapping of (Net-Str b₂) = id b₂ & the carrier of (Net-Str b₂) = b₂ & Net-Str b₂ is full SubRelStr of b₁ )

proof end;

theorem Th33: :: WAYBEL21:33

for b₁, b₂ being non empty up-complete Poset
for b₃ being monotone Function of b₁,b₂
for b₄ being non empty directed Subset of b₁ holds lim_inf (b₃ * (Net-Str b₄)) = sup (b₃ .: b₄)

proof end;

theorem Th34: :: WAYBEL21:34

for b₁ being non empty reflexive RelStr
for b₂ being non empty directed Subset of b₁
for b₃, b₄ being Element of (Net-Str b₂) holds
( b₃ <= b₄ iff (Net-Str b₂) . b₃ <= (Net-Str b₂) . b₄ )

proof end;

theorem Th35: :: WAYBEL21:35

for b₁ being complete Lawson TopLattice
for b₂ being non empty directed Subset of b₁ holds sup b₂ in Lim (Net-Str b₂)

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
let c₃ be non empty NetStr of c₁;
assume E25: c₃ is subnet of c₂ ;
mode Embedding of c₃,c₂ -> Function of a₃,a₂ means :Def3: :: WAYBEL21:def 3
( the mapping of a₃ = the mapping of a₂ * a₄ & ( for b₁ being Element of a₂ ex b₂ being Element of a₃ st
for b₃ being Element of a₃ st b₂ <= b₃ holds
b₁ <= a₄ . b₃ ) );
existence by E25, YELLOW_6:def 12;

end;

:: deftheorem Def3 defines Embedding WAYBEL21:def 3 :

theorem Th36: :: WAYBEL21:36

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being non empty subnet of b₂
for b₄ being Embedding of b₃,b₂
for b₅ being Element of b₃ holds b₃ . b₅ = b₂ . (b₄ . b₅)

proof end;

theorem Th37: :: WAYBEL21:37

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being subnet of b₂ holds lim_inf b₂ <= lim_inf b₃

proof end;

theorem Th38: :: WAYBEL21:38

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being subnet of b₂
for b₄ being Embedding of b₃,b₂ st ( for b₅ being Element of b₂
for b₆ being Element of b₃ st b₄ . b₆ <= b₅ holds
ex b₇ being Element of b₃ st
( b₇ >= b₆ & b₂ . b₅ >= b₃ . b₇ ) ) holds
lim_inf b₂ = lim_inf b₃

proof end;

theorem Th39: :: WAYBEL21:39

for b₁ being non empty RelStr
for b₂ being net of b₁
for b₃ being non empty full SubNetStr of b₂ st ( for b₄ being Element of b₂ ex b₅ being Element of b₂ st
( b₅ >= b₄ & b₅ in the carrier of b₃ ) ) holds
( b₃ is subnet of b₂ & incl b₃,b₂ is Embedding of b₃,b₂ )

proof end;

theorem Th40: :: WAYBEL21:40

for b₁ being non empty RelStr
for b₂ being net of b₁
for b₃ being Element of b₂ holds
( b₂ | b₃ is subnet of b₂ & incl (b₂ | b₃),b₂ is Embedding of b₂ | b₃,b₂ )

proof end;

theorem Th41: :: WAYBEL21:41

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Element of b₂ holds lim_inf (b₂ | b₃) = lim_inf b₂

proof end;

theorem Th42: :: WAYBEL21:42

for b₁ being non empty RelStr
for b₂ being net of b₁
for b₃ being set st b₂ is_eventually_in b₃ holds
ex b₄ being Element of b₂ st
( b₂ . b₄ in b₃ & rng the mapping of (b₂ | b₄) c= b₃ )

proof end;

theorem Th43: :: WAYBEL21:43

for b₁ being complete Lawson TopLattice
for b₂ being eventually-filtered net of b₁ holds rng the mapping of b₂ is non empty filtered Subset of b₁

proof end;

theorem Th44: :: WAYBEL21:44

for b₁ being complete Lawson TopLattice
for b₂ being eventually-filtered net of b₁ holds Lim b₂ = {(inf b₂)}

proof end;

theorem Th45: :: WAYBEL21:45

for b₁, b₂ being complete Lawson TopLattice
for b₃ being meet-preserving Function of b₁,b₂ holds
( b₃ is continuous iff ( b₃ is directed-sups-preserving & ( for b₄ being non empty Subset of b₁ holds b₃ preserves_inf_of b₄ ) ) )

proof end;

theorem Th46: :: WAYBEL21:46

for b₁, b₂ being complete Lawson TopLattice
for b₃ being SemilatticeHomomorphism of b₁,b₂ holds
( b₃ is continuous iff ( b₃ is infs-preserving & b₃ is directed-sups-preserving ) )

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is lim_infs-preserving means :: WAYBEL21:def 4
for b₁ being net of a₁ holds a₃ . (lim_inf b₁) = lim_inf (a₃ * b₁);

end;

:: deftheorem Def4 defines lim_infs-preserving WAYBEL21:def 4 :

theorem Th47: :: WAYBEL21:47

for b₁, b₂ being complete Lawson TopLattice
for b₃ being SemilatticeHomomorphism of b₁,b₂ holds
( b₃ is continuous iff b₃ is lim_infs-preserving )

proof end;

theorem Th48: :: WAYBEL21:48

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full meet-inheriting SubRelStr of b₁ st Top b₁ in the carrier of b₂ & ex b₃ being Subset of b₁ st
( b₃ = the carrier of b₂ & b₃ is closed ) holds
b₂ is infs-inheriting

proof end;

theorem Th49: :: WAYBEL21:49

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full SubRelStr of b₁ st ex b₃ being Subset of b₁ st
( b₃ = the carrier of b₂ & b₃ is closed ) holds
b₂ is directed-sups-inheriting

proof end;

theorem Th50: :: WAYBEL21:50

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full infs-inheriting directed-sups-inheriting SubRelStr of b₁ ex b₃ being Subset of b₁ st
( b₃ = the carrier of b₂ & b₃ is closed )

proof end;

theorem Th51: :: WAYBEL21:51

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full infs-inheriting directed-sups-inheriting SubRelStr of b₁
for b₃ being net of b₁ st b₃ is_eventually_in the carrier of b₂ holds
lim_inf b₃ in the carrier of b₂

proof end;

theorem Th52: :: WAYBEL21:52

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full meet-inheriting SubRelStr of b₁ st Top b₁ in the carrier of b₂ & ( for b₃ being net of b₁ st rng the mapping of b₃ c= the carrier of b₂ holds
lim_inf b₃ in the carrier of b₂ ) holds
b₂ is infs-inheriting

proof end;

theorem Th53: :: WAYBEL21:53

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full SubRelStr of b₁ st ( for b₃ being net of b₁ st rng the mapping of b₃ c= the carrier of b₂ holds
lim_inf b₃ in the carrier of b₂ ) holds
b₂ is directed-sups-inheriting

proof end;

theorem Th54: :: WAYBEL21:54

for b₁ being continuous complete Lawson TopLattice
for b₂ being non empty full meet-inheriting SubRelStr of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ & Top b₁ in b₃ holds
( b₃ is closed iff for b₄ being net of b₁ st b₄ is_eventually_in b₃ holds
lim_inf b₄ in b₃ )

proof end;