:: WAYBEL24 semantic presentation

theorem Th1: :: WAYBEL24:1

for b₁, b₂ being up-complete Scott TopLattice
for b₃ being Subset of (SCMaps b₁,b₂) holds "\/" b₃,(SCMaps b₁,b₂) is continuous Function of b₁,b₂

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive RelStr ;
cluster constant -> monotone M4(the carrier of a₁,the carrier of a₂);
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive RelStr ;
let c₃ be Element of c₂;
cluster a₁ --> a₃ -> monotone ;
coherence

proof end;

end;

theorem Th2: :: WAYBEL24:2

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps b₁,b₂) = b₁ --> (Bottom b₂)

proof end;

theorem Th3: :: WAYBEL24:3

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps b₁,b₂) = b₁ --> (Top b₂)

proof end;

scheme :: WAYBEL24:sch 1
s1{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , F₃( set ) -> Element of F₂(), F₄() -> Function, P₁[ set ] } :

F₄() .: { F₃(b₁) where B is Element of F₁() : P₁[b₁] } = { (F₄() . F₃(b₁)) where B is Element of F₁() : P₁[b₁] }

provided

E1: the carrier of F₂() c= dom F₄()

proof end;

scheme :: WAYBEL24:sch 2
s2{ F₁() -> LATTICE, F₂( set ) -> set , P₁[ set ], P₂[ set ] } :

{ F₂(b₁) where B is Element of F₁() : P₁[b₁] } = { F₂(b₁) where B is Element of F₁() : P₂[b₁] }

provided

E1: for b₁ being Element of F₁() holds
( P₁[b₁] iff P₂[b₁] )

proof end;

theorem Th4: :: WAYBEL24:4

for b₁, b₂ being complete LATTICE
for b₃ being monotone Function of b₁,b₂
for b₄ being Element of b₁ holds b₃ . b₄ = sup (b₃ .: (downarrow b₄))

proof end;

theorem Th5: :: WAYBEL24:5

for b₁, b₂ being lower-bounded complete LATTICE
for b₃ being monotone Function of b₁,b₂
for b₄ being Element of b₁ holds b₃ . b₄ = "\/" { (b₃ . b₅) where B is Element of b₁ : b₅ <= b₄ } ,b₂

proof end;

theorem Th6: :: WAYBEL24:6

for b₁ being RelStr
for b₂ being non empty RelStr
for b₃ being Subset of (b₂ |^ the carrier of b₁) holds sup b₃ is Function of b₁,b₂

proof end;

definition

let c₁, c₂, c₃ be non empty RelStr ;
let c₄ be Function of [:c₁,c₂:],c₃;
let c₅ be Element of c₁;
func Proj c₄,c₅ -> Function of a₂,a₃ equals :: WAYBEL24:def 1
(curry a₄) . a₅;
correctness

proof end;

end;

:: deftheorem Def1 defines Proj WAYBEL24:def 1 :

theorem Th7: :: WAYBEL24:7

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of [:b₂,b₃:],b₁
for b₅ being Element of b₂
for b₆ being Element of b₃ holds (Proj b₄,b₅) . b₆ = b₄ . [b₅,b₆]

proof end;

definition

let c₁, c₂, c₃ be non empty RelStr ;
let c₄ be Function of [:c₁,c₂:],c₃;
let c₅ be Element of c₂;
func Proj c₄,c₅ -> Function of a₁,a₃ equals :: WAYBEL24:def 2
(curry' a₄) . a₅;
correctness

proof end;

end;

:: deftheorem Def2 defines Proj WAYBEL24:def 2 :

theorem Th8: :: WAYBEL24:8

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of [:b₃,b₂:],b₁
for b₅ being Element of b₂
for b₆ being Element of b₃ holds (Proj b₄,b₅) . b₆ = b₄ . [b₆,b₅]

proof end;

theorem Th9: :: WAYBEL24:9

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being Element of b₁
for b₆ being Element of b₂ holds (Proj b₄,b₅) . b₆ = (Proj b₄,b₆) . b₅

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive RelStr ;
cluster antitone M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

theorem Th10: :: WAYBEL24:10

for b₁, b₂, b₃ being non empty reflexive RelStr
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being Element of b₁
for b₆ being Element of b₂ st b₄ is monotone holds
( Proj b₄,b₅ is monotone & Proj b₄,b₆ is monotone )

proof end;

theorem Th11: :: WAYBEL24:11

for b₁, b₂, b₃ being non empty reflexive RelStr
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being Element of b₁
for b₆ being Element of b₂ st b₄ is antitone holds
( Proj b₄,b₅ is antitone & Proj b₄,b₆ is antitone )

proof end;

registration

let c₁, c₂, c₃ be non empty reflexive RelStr ;
let c₄ be monotone Function of [:c₁,c₂:],c₃;
let c₅ be Element of c₁;
cluster Proj a₄,a₅ -> monotone ;
coherence by Th10;

end;

registration

let c₁, c₂, c₃ be non empty reflexive RelStr ;
let c₄ be monotone Function of [:c₁,c₂:],c₃;
let c₅ be Element of c₂;
cluster Proj a₄,a₅ -> monotone ;
coherence by Th10;

end;

registration

let c₁, c₂, c₃ be non empty reflexive RelStr ;
let c₄ be antitone Function of [:c₁,c₂:],c₃;
let c₅ be Element of c₁;
cluster Proj a₄,a₅ -> antitone ;
coherence by Th11;

end;

registration

let c₁, c₂, c₃ be non empty reflexive RelStr ;
let c₄ be antitone Function of [:c₁,c₂:],c₃;
let c₅ be Element of c₂;
cluster Proj a₄,a₅ -> antitone ;
coherence by Th11;

end;

theorem Th12: :: WAYBEL24:12

for b₁, b₂, b₃ being LATTICE
for b₄ being Function of [:b₁,b₂:],b₃ st ( for b₅ being Element of b₁
for b₆ being Element of b₂ holds
( Proj b₄,b₅ is monotone & Proj b₄,b₆ is monotone ) ) holds
b₄ is monotone

proof end;

theorem Th13: :: WAYBEL24:13

for b₁, b₂, b₃ being LATTICE
for b₄ being Function of [:b₁,b₂:],b₃ st ( for b₅ being Element of b₁
for b₆ being Element of b₂ holds
( Proj b₄,b₅ is antitone & Proj b₄,b₆ is antitone ) ) holds
b₄ is antitone

proof end;

theorem Th14: :: WAYBEL24:14

for b₁, b₂, b₃ being LATTICE
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being Element of b₂
for b₆ being Subset of b₁ holds (Proj b₄,b₅) .: b₆ = b₄ .: [:b₆,{b₅}:]

proof end;

theorem Th15: :: WAYBEL24:15

for b₁, b₂, b₃ being LATTICE
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being Element of b₁
for b₆ being Subset of b₂ holds (Proj b₄,b₅) .: b₆ = b₄ .: [:{b₅},b₆:]

proof end;

theorem Th16: :: WAYBEL24:16

for b₁, b₂, b₃ being LATTICE
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being Element of b₁
for b₆ being Element of b₂ st b₄ is directed-sups-preserving holds
( Proj b₄,b₅ is directed-sups-preserving & Proj b₄,b₆ is directed-sups-preserving )

proof end;

theorem Th17: :: WAYBEL24:17

for b₁, b₂, b₃ being LATTICE
for b₄ being monotone Function of [:b₁,b₂:],b₃
for b₅ being Element of b₁
for b₆ being Element of b₂
for b₇ being directed Subset of [:b₁,b₂:] st ex_sup_of b₄ .: b₇,b₃ & b₅ in proj1 b₇ & b₆ in proj2 b₇ holds
b₄ . [b₅,b₆] <= sup (b₄ .: b₇)

proof end;

theorem Th18: :: WAYBEL24:18

for b₁, b₂, b₃ being complete LATTICE
for b₄ being Function of [:b₁,b₂:],b₃ st ( for b₅ being Element of b₁
for b₆ being Element of b₂ holds
( Proj b₄,b₅ is directed-sups-preserving & Proj b₄,b₆ is directed-sups-preserving ) ) holds
b₄ is directed-sups-preserving

proof end;

theorem Th19: :: WAYBEL24:19

for b₁ being set
for b₂ being non empty RelStr
for b₃ being set holds
( b₃ is Element of (b₂ |^ b₁) iff b₃ is Function of b₁,the carrier of b₂ )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be non empty TopRelStr ;
func ContMaps c₁,c₂ -> strict RelStr means :Def3: :: WAYBEL24:def 3
( a₃ is full SubRelStr of a₂ |^ the carrier of a₁ & ( for b₁ being set holds
( b₁ in the carrier of a₃ iff ex b₂ being Function of a₁,a₂ st
( b₁ = b₂ & b₂ is continuous ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ContMaps WAYBEL24:def 3 :

registration

let c₁ be non empty TopSpace;
let c₂ be non empty TopSpace-like TopRelStr ;
cluster ContMaps a₁,a₂ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty TopSpace-like TopRelStr ;
cluster ContMaps a₁,a₂ -> non empty strict constituted-Functions ;
coherence

proof end;

end;

theorem Th20: :: WAYBEL24:20

for b₁ being non empty TopSpace
for b₂ being non empty reflexive TopSpace-like TopRelStr
for b₃, b₄ being Element of (ContMaps b₁,b₂) holds
( b₃ <= b₄ iff for b₅ being Element of b₁ holds [(b₃ . b₅),(b₄ . b₅)] in the InternalRel of b₂ )

proof end;

theorem Th21: :: WAYBEL24:21

for b₁ being non empty TopSpace
for b₂ being non empty reflexive TopSpace-like TopRelStr
for b₃ being set holds
( b₃ is continuous Function of b₁,b₂ iff b₃ is Element of (ContMaps b₁,b₂) )

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty reflexive TopSpace-like TopRelStr ;
cluster ContMaps a₁,a₂ -> non empty strict reflexive constituted-Functions ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty transitive TopSpace-like TopRelStr ;
cluster ContMaps a₁,a₂ -> non empty strict transitive constituted-Functions ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty antisymmetric TopSpace-like TopRelStr ;
cluster ContMaps a₁,a₂ -> non empty strict antisymmetric constituted-Functions ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty RelStr ;
cluster a₂ |^ a₁ -> constituted-Functions ;
coherence

proof end;

end;

theorem Th22: :: WAYBEL24:22

for b₁ being non empty 1-sorted
for b₂ being complete LATTICE
for b₃, b₄, b₅ being Function of b₁,b₂
for b₆ being Element of b₁ st b₅ = "\/" {b₃,b₄},(b₂ |^ the carrier of b₁) holds
b₅ . b₆ = sup {(b₃ . b₆),(b₄ . b₆)}

proof end;

theorem Th23: :: WAYBEL24:23

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is complete LATTICE ) holds
for b₃ being Subset of (product b₂)
for b₄ being Element of b₁ holds (inf b₃) . b₄ = inf (pi b₃,b₄)

proof end;

theorem Th24: :: WAYBEL24:24

for b₁ being non empty 1-sorted
for b₂ being complete LATTICE
for b₃, b₄, b₅ being Function of b₁,b₂
for b₆ being Element of b₁ st b₅ = "/\" {b₃,b₄},(b₂ |^ the carrier of b₁) holds
b₅ . b₆ = inf {(b₃ . b₆),(b₄ . b₆)}

proof end;

theorem Th25: :: WAYBEL24:25

for b₁ being non empty RelStr
for b₂ being complete LATTICE
for b₃ being non empty Subset of (b₂ |^ the carrier of b₁)
for b₄ being Element of b₁ holds (sup b₃) . b₄ = "\/" { (b₅ . b₄) where B is Element of (b₂ |^ the carrier of b₁) : b₅ in b₃ } ,b₂

proof end;

theorem Th26: :: WAYBEL24:26

for b₁, b₂ being complete TopLattice
for b₃ being non empty Subset of (ContMaps b₁,b₂)
for b₄ being Element of b₁ holds ("\/" b₃,(b₂ |^ the carrier of b₁)) . b₄ = "\/" { (b₅ . b₄) where B is Element of (b₂ |^ the carrier of b₁) : b₅ in b₃ } ,b₂

proof end;

theorem Th27: :: WAYBEL24:27

for b₁ being non empty RelStr
for b₂ being complete LATTICE
for b₃ being non empty Subset of (b₂ |^ the carrier of b₁)
for b₄ being non empty Subset of b₁ holds (sup b₃) .: b₄ = { ("\/" { (b₆ . b₅) where B is Element of (b₂ |^ the carrier of b₁) : b₆ in b₃ } ,b₂) where B is Element of b₁ : b₅ in b₄ }

proof end;

theorem Th28: :: WAYBEL24:28

for b₁, b₂ being Scott complete TopLattice
for b₃ being non empty Subset of (ContMaps b₁,b₂)
for b₄ being non empty Subset of b₁ holds ("\/" b₃,(b₂ |^ the carrier of b₁)) .: b₄ = { ("\/" { (b₆ . b₅) where B is Element of (b₂ |^ the carrier of b₁) : b₆ in b₃ } ,b₂) where B is Element of b₁ : b₅ in b₄ }

proof end;

scheme :: WAYBEL24:sch 3
s3{ F₁() -> non empty TopRelStr , F₂( set ) -> set , F₃( set ) -> set , P₁[ set ] } :

{ F₂(b₁) where B is Element of F₁() : P₁[b₁] } = { F₃(b₁) where B is Element of F₁() : P₁[b₁] }

provided

E21: for b₁ being Element of F₁() st P₁[b₁] holds
F₂(b₁) = F₃(b₁)

proof end;

scheme :: WAYBEL24:sch 4
s4{ F₁() -> non empty RelStr , F₂( set ) -> set , F₃( set ) -> set , P₁[ set ] } :

{ F₂(b₁) where B is Element of F₁() : P₁[b₁] } = { F₃(b₁) where B is Element of F₁() : P₁[b₁] }

provided

E21: for b₁ being Element of F₁() st P₁[b₁] holds
F₂(b₁) = F₃(b₁)

proof end;

scheme :: WAYBEL24:sch 5
s5{ F₁() -> non empty TopRelStr , F₂() -> non empty TopRelStr , F₃( set ) -> Element of F₂(), F₄() -> Function, P₁[ set ] } :

F₄() .: { F₃(b₁) where B is Element of F₁() : P₁[b₁] } = { (F₄() . F₃(b₁)) where B is Element of F₁() : P₁[b₁] }

provided

E21: the carrier of F₂() c= dom F₄()

proof end;

Lemma21: for b₁ being non empty RelStr
for b₂ being non empty Subset of b₁ holds b₂ = { b₃ where B is Element of b₁ : b₃ in b₂ }

proof end;

theorem Th29: :: WAYBEL24:29

for b₁, b₂ being Scott complete TopLattice
for b₃ being non empty Subset of (ContMaps b₁,b₂) holds "\/" b₃,(b₂ |^ the carrier of b₁) is monotone Function of b₁,b₂

proof end;

theorem Th30: :: WAYBEL24:30

for b₁, b₂ being Scott complete TopLattice
for b₃ being non empty Subset of (ContMaps b₁,b₂)
for b₄ being non empty directed Subset of b₁ holds "\/" { ("\/" { (b₅ . b₆) where B is Element of b₁ : b₆ in b₄ } ,b₂) where B is Element of (b₂ |^ the carrier of b₁) : b₅ in b₃ } ,b₂ = "\/" { ("\/" { (b₆ . b₅) where B is Element of (b₂ |^ the carrier of b₁) : b₆ in b₃ } ,b₂) where B is Element of b₁ : b₅ in b₄ } ,b₂

proof end;

theorem Th31: :: WAYBEL24:31

for b₁, b₂ being Scott complete TopLattice
for b₃ being non empty Subset of (ContMaps b₁,b₂)
for b₄ being non empty directed Subset of b₁ holds "\/" (("\/" b₃,(b₂ |^ the carrier of b₁)) .: b₄),b₂ = ("\/" b₃,(b₂ |^ the carrier of b₁)) . (sup b₄)

proof end;

theorem Th32: :: WAYBEL24:32

for b₁, b₂ being Scott complete TopLattice
for b₃ being non empty Subset of (ContMaps b₁,b₂) holds "\/" b₃,(b₂ |^ the carrier of b₁) in the carrier of (ContMaps b₁,b₂)

proof end;

theorem Th33: :: WAYBEL24:33

for b₁ being non empty RelStr
for b₂ being non empty antisymmetric lower-bounded RelStr holds Bottom (b₂ |^ the carrier of b₁) = b₁ --> (Bottom b₂)

proof end;

theorem Th34: :: WAYBEL24:34

for b₁ being non empty RelStr
for b₂ being non empty antisymmetric upper-bounded RelStr holds Top (b₂ |^ the carrier of b₁) = b₁ --> (Top b₂)

proof end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be complete LATTICE;
let c₃ be Element of c₂;
cluster a₁ --> a₃ -> monotone directed-sups-preserving ;
coherence

proof end;

end;

theorem Th35: :: WAYBEL24:35

for b₁, b₂ being Scott complete TopLattice holds ContMaps b₁,b₂ is sups-inheriting SubRelStr of b₂ |^ the carrier of b₁

proof end;

registration

let c₁, c₂ be Scott complete TopLattice;
cluster ContMaps a₁,a₂ -> non empty strict reflexive transitive antisymmetric complete constituted-Functions ;
coherence

proof end;

end;

theorem Th36: :: WAYBEL24:36

for b₁, b₂ being non empty Scott complete TopLattice holds Bottom (ContMaps b₁,b₂) = b₁ --> (Bottom b₂)

proof end;

theorem Th37: :: WAYBEL24:37

for b₁, b₂ being non empty Scott complete TopLattice holds Top (ContMaps b₁,b₂) = b₁ --> (Top b₂)

proof end;

theorem Th38: :: WAYBEL24:38

for b₁, b₂ being Scott complete TopLattice holds SCMaps b₁,b₂ = ContMaps b₁,b₂

proof end;