:: WAYBEL29 semantic presentation

theorem Th1: :: WAYBEL29:1

for b₁, b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂ st b₃ is one-to-one & b₃ is onto holds
( b₃ * (b₃ " ) = id b₂ & (b₃ " ) * b₃ = id b₁ & b₃ " is one-to-one & b₃ " is onto )

proof end;

theorem Th2: :: WAYBEL29:2

for b₁, b₂ being non empty set
for b₃ being non empty RelStr
for b₄ being non empty SubRelStr of b₃ |^ [:b₁,b₂:]
for b₅ being non empty SubRelStr of (b₃ |^ b₂) |^ b₁
for b₆ being Function of b₄,b₅ st b₆ is currying & b₆ is one-to-one & b₆ is onto holds
b₆ " is uncurrying

proof end;

theorem Th3: :: WAYBEL29:3

for b₁, b₂ being non empty set
for b₃ being non empty RelStr
for b₄ being non empty SubRelStr of b₃ |^ [:b₁,b₂:]
for b₅ being non empty SubRelStr of (b₃ |^ b₂) |^ b₁
for b₆ being Function of b₅,b₄ st b₆ is uncurrying & b₆ is one-to-one & b₆ is onto holds
b₆ " is currying

proof end;

theorem Th4: :: WAYBEL29:4

for b₁, b₂ being non empty set
for b₃ being non empty Poset
for b₄ being non empty full SubRelStr of b₃ |^ [:b₁,b₂:]
for b₅ being non empty full SubRelStr of (b₃ |^ b₂) |^ b₁
for b₆ being Function of b₄,b₅ st b₆ is currying & b₆ is one-to-one & b₆ is onto holds
b₆ is isomorphic

proof end;

theorem Th5: :: WAYBEL29:5

for b₁, b₂ being non empty set
for b₃ being non empty Poset
for b₄ being non empty full SubRelStr of b₃ |^ [:b₁,b₂:]
for b₅ being non empty full SubRelStr of (b₃ |^ b₂) |^ b₁
for b₆ being Function of b₅,b₄ st b₆ is uncurrying & b₆ is one-to-one & b₆ is onto holds
b₆ is isomorphic

proof end;

theorem Th6: :: WAYBEL29:6

for b₁, b₂, b₃, b₄ being 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₃ st b₅ is isomorphic holds
for b₆ being Function of b₂,b₄ st b₆ = b₅ holds
b₆ is isomorphic

proof end;

theorem Th7: :: WAYBEL29:7

for b₁, b₂, b₃ being RelStr
for b₄ being Function of b₁,b₂ st b₄ is isomorphic holds
for b₅ being Function of b₂,b₃ st b₅ is isomorphic holds
for b₆ being Function of b₁,b₃ st b₆ = b₅ * b₄ holds
b₆ is isomorphic

proof end;

theorem Th8: :: WAYBEL29:8

canceled;

theorem Th9: :: WAYBEL29:9

canceled;

theorem Th10: :: WAYBEL29:10

for b₁, b₂, b₃, b₄ being TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₃,the topology of b₃ #) & TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of b₄,the topology of b₄ #) holds
[:b₁,b₂:] = [:b₃,b₄:]

proof end;

theorem Th11: :: WAYBEL29:11

for b₁ being non empty TopSpace
for b₂ being non empty up-complete Scott TopPoset
for b₃ being non empty directed Subset of (ContMaps b₁,b₂) holds "\/" b₃,(b₂ |^ the carrier of b₁) is continuous Function of b₁,b₂

proof end;

theorem Th12: :: WAYBEL29:12

for b₁ being non empty TopSpace
for b₂ being non empty up-complete Scott TopPoset holds ContMaps b₁,b₂ is directed-sups-inheriting SubRelStr of b₂ |^ the carrier of b₁

proof end;

theorem Th13: :: WAYBEL29:13

for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
for b₃, b₄ being non empty TopRelStr st TopRelStr(# the carrier of b₃,the InternalRel of b₃,the topology of b₃ #) = TopRelStr(# the carrier of b₄,the InternalRel of b₄,the topology of b₄ #) holds
ContMaps b₁,b₃ = ContMaps b₂,b₄

proof end;

registration

cluster Scott complete continuous -> complete continuous injective T_0 TopRelStr ;
coherence

proof end;

end;

registration

cluster Scott complete continuous injective T_0 TopRelStr ;
existence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty up-complete Scott TopPoset;
cluster ContMaps a₁,a₂ -> up-complete ;
coherence

proof end;

end;

theorem Th14: :: WAYBEL29:14

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is up-complete ) holds
b₁ -POS_prod b₂ is up-complete

proof end;

theorem Th15: :: WAYBEL29:15

for b₁ being non empty set
for b₂ being non-Empty reflexive-yielding Poset-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds
( b₂ . b₃ is up-complete & b₂ . b₃ is lower-bounded ) ) holds
for b₃, b₄ being Element of (product b₂) holds
( b₃ << b₄ iff ( ( for b₅ being Element of b₁ holds b₃ . b₅ << b₄ . b₅ ) & ex b₅ being finite Subset of b₁ st
for b₆ being Element of b₁ st not b₆ in b₅ holds
b₃ . b₆ = Bottom (b₂ . b₆) ) )

proof end;

registration

let c₁ be set ;
let c₂ be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster a₂ |^ a₁ -> lower-bounded ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty lower-bounded TopPoset;
cluster ContMaps a₁,a₂ -> lower-bounded ;
coherence

proof end;

end;

registration

let c₁ be non empty up-complete Poset;
cluster -> up-complete TopAugmentation of a₁;
coherence

proof end;

cluster Scott -> correct TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty up-complete Poset;
cluster up-complete correct strict Scott TopAugmentation of a₁;
existence

proof end;

end;

theorem Th16: :: WAYBEL29:16

canceled;

theorem Th17: :: WAYBEL29:17

for b₁ being non empty up-complete Poset
for b₂, b₃ being Scott TopAugmentation of b₁ holds the topology of b₂ = the topology of b₃

proof end;

theorem Th18: :: WAYBEL29:18

for b₁, b₂ being non empty reflexive antisymmetric up-complete TopRelStr st TopRelStr(# the carrier of b₁,the InternalRel of b₁,the topology of b₁ #) = TopRelStr(# the carrier of b₂,the InternalRel of b₂,the topology of b₂ #) & b₁ is Scott holds
b₂ is Scott

proof end;

definition

let c₁ be non empty up-complete Poset;
func Sigma c₁ -> strict Scott TopAugmentation of a₁ means :Def1: :: WAYBEL29:def 1
verum;
uniqueness

proof end;

existence ;

end;

:: deftheorem Def1 defines Sigma WAYBEL29:def 1 :

theorem Th19: :: WAYBEL29:19

for b₁ being non empty up-complete Scott TopPoset holds Sigma b₁ = TopRelStr(# the carrier of b₁,the InternalRel of b₁,the topology of b₁ #)

proof end;

theorem Th20: :: WAYBEL29:20

for b₁, b₂ being non empty up-complete Poset st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
Sigma b₁ = Sigma b₂

proof end;

definition

let c₁, c₂ be non empty up-complete Poset;
let c₃ be Function of c₁,c₂;
func Sigma c₃ -> Function of (Sigma a₁),(Sigma a₂) equals :: WAYBEL29:def 2
a₃;
coherence

proof end;

end;

:: deftheorem Def2 defines Sigma WAYBEL29:def 2 :

registration

let c₁, c₂ be non empty up-complete Poset;
let c₃ be directed-sups-preserving Function of c₁,c₂;
cluster Sigma a₃ -> continuous ;
coherence

proof end;

end;

theorem Th21: :: WAYBEL29:21

for b₁, b₂ being non empty up-complete Poset
for b₃ being Function of b₁,b₂ holds
( b₃ is isomorphic iff Sigma b₃ is isomorphic )

proof end;

theorem Th22: :: WAYBEL29:22

for b₁ being non empty TopSpace
for b₂ being Scott complete TopLattice holds oContMaps b₁,b₂ = ContMaps b₁,b₂

proof end;

definition

let c₁, c₂ be non empty TopSpace;
func Theta c₁,c₂ -> Function of (InclPoset the topology of [:a₁,a₂:]),(ContMaps a₁,(Sigma (InclPoset the topology of a₂))) means :Def3: :: WAYBEL29:def 3
for b₁ being open Subset of [:a₁,a₂:] holds a₃ . b₁ = b₁,the carrier of a₁ *graph ;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines Theta WAYBEL29:def 3 :

defpred S₁[ T_0-TopSpace] means for b₁ being non empty TopSpace
for b₂ being Scott complete continuous TopLattice
for b₃ being Scott TopAugmentation of ContMaps a₁,b₂ ex b₄ being Function of (ContMaps b₁,b₃),(ContMaps [:b₁,a₁:],b₂)ex b₅ being Function of (ContMaps [:b₁,a₁:],b₂),(ContMaps b₁,b₃) st
( b₄ is uncurrying & b₄ is one-to-one & b₄ is onto & b₅ is currying & b₅ is one-to-one & b₅ is onto );

defpred S₂[ T_0-TopSpace] means for b₁ being non empty TopSpace
for b₂ being Scott complete continuous TopLattice
for b₃ being Scott TopAugmentation of ContMaps a₁,b₂ ex b₄ being Function of (ContMaps b₁,b₃),(ContMaps [:b₁,a₁:],b₂)ex b₅ being Function of (ContMaps [:b₁,a₁:],b₂),(ContMaps b₁,b₃) st
( b₄ is uncurrying & b₄ is isomorphic & b₅ is currying & b₅ is isomorphic );

defpred S₃[ T_0-TopSpace] means for b₁ being non empty TopSpace holds Theta b₁,a₁ is isomorphic;

defpred S₄[ T_0-TopSpace] means for b₁ being non empty TopSpace
for b₂ being Scott TopAugmentation of InclPoset the topology of a₁
for b₃ being continuous Function of b₁,b₂ holds *graph b₃ is open Subset of [:b₁,a₁:];

defpred S₅[ T_0-TopSpace] means for b₁ being Scott TopAugmentation of InclPoset the topology of a₁ holds { [b₂,b₃] where B is open Subset of a₁, B is Element of a₁ : b₃ in b₂ } is open Subset of [:b₁,a₁:];

defpred S₆[ T_0-TopSpace] means for b₁ being Scott TopAugmentation of InclPoset the topology of a₁
for b₂ being Element of a₁
for b₃ being open a_neighborhood of b₂ ex b₄ being open Subset of b₁ st
( b₃ in b₄ & meet b₄ is a_neighborhood of b₂ );

Lemma18: for b₁ being T_0-TopSpace holds
( S₁[b₁] iff S₂[b₁] )

proof end;

definition

let c₁ be non empty TopSpace;
func alpha c₁ -> Function of (oContMaps a₁,Sierpinski_Space ),(InclPoset the topology of a₁) means :Def4: :: WAYBEL29:def 4
for b₁ being continuous Function of a₁,Sierpinski_Space holds a₂ . b₁ = b₁ " {1};
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines alpha WAYBEL29:def 4 :

theorem Th23: :: WAYBEL29:23

for b₁ being non empty TopSpace
for b₂ being open Subset of b₁ holds ((alpha b₁) " ) . b₂ = chi b₂,the carrier of b₁

proof end;

registration

let c₁ be non empty TopSpace;
cluster alpha a₁ -> isomorphic ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster (alpha a₁) " -> isomorphic ;
coherence by YELLOW14:11;

end;

registration

let c₁ be injective T_0-TopSpace;
cluster Omega a₁ -> Scott injective T_0 ;
coherence

proof end;

end;

registration

let c₁ be non empty TopSpace;
cluster oContMaps a₁,Sierpinski_Space -> complete ;
coherence

proof end;

end;

theorem Th24: :: WAYBEL29:24

Omega Sierpinski_Space = Sigma (BoolePoset 1)

proof end;

registration

let c₁ be non empty set ;
let c₂ be injective T_0-TopSpace;
cluster product (a₁ => a₂) -> injective ;
coherence

proof end;

end;

theorem Th25: :: WAYBEL29:25

for b₁ being non empty set
for b₂ being complete continuous LATTICE holds Omega (b₁ -TOP_prod (b₁ => (Sigma b₂))) = Sigma (b₁ -POS_prod (b₁ => b₂))

proof end;

theorem Th26: :: WAYBEL29:26

for b₁ being non empty set
for b₂ being injective T_0-TopSpace holds Omega (b₁ -TOP_prod (b₁ => b₂)) = Sigma (b₁ -POS_prod (b₁ => (Omega b₂)))

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be non empty TopSpace;
func commute c₂,c₁,c₃ -> Function of (oContMaps a₂,(a₁ -TOP_prod (a₁ => a₃))),((oContMaps a₂,a₃) |^ a₁) means :Def5: :: WAYBEL29:def 5
for b₁ being continuous Function of a₂,(a₁ -TOP_prod (a₁ => a₃)) holds a₄ . b₁ = commute b₁;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def5 defines commute WAYBEL29:def 5 :

registration

let c₁ be non empty set ;
let c₂, c₃ be non empty TopSpace;
cluster commute a₂,a₁,a₃ -> V5 onto ;
correctness

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty TopSpace;
cluster commute a₂,a₁,Sierpinski_Space -> V5 onto isomorphic ;
correctness

proof end;

end;

Lemma21: for b₁ being T_0-TopSpace st S₃[b₁] holds
S₄[b₁]

proof end;

theorem Th27: :: WAYBEL29:27

for b₁, b₂ being non empty TopSpace
for b₃ being Scott TopAugmentation of InclPoset the topology of b₂
for b₄, b₅ being Element of (ContMaps b₁,b₃) st b₄ <= b₅ holds
*graph b₄ c= *graph b₅

proof end;

Lemma23: for b₁ being T_0-TopSpace st S₄[b₁] holds
S₃[b₁]

proof end;

Lemma24: for b₁ being T_0-TopSpace st S₄[b₁] holds
S₅[b₁]

proof end;

Lemma25: for b₁ being T_0-TopSpace st S₅[b₁] holds
S₆[b₁]

proof end;

Lemma26: for b₁ being T_0-TopSpace st S₆[b₁] holds
S₄[b₁]

proof end;

Lemma27: for b₁ being T_0-TopSpace st S₆[b₁] holds
InclPoset the topology of b₁ is continuous

proof end;

Lemma28: for b₁ being T_0-TopSpace st InclPoset the topology of b₁ is continuous holds
S₆[b₁]

proof end;

theorem Th28: :: WAYBEL29:28

for b₁ being T_0-TopSpace holds
( ( for b₂ being non empty TopSpace
for b₃ being Scott complete continuous TopLattice
for b₄ being Scott TopAugmentation of ContMaps b₁,b₃ ex b₅ being Function of (ContMaps b₂,b₄),(ContMaps [:b₂,b₁:],b₃)ex b₆ being Function of (ContMaps [:b₂,b₁:],b₃),(ContMaps b₂,b₄) st
( b₅ is uncurrying & b₅ is one-to-one & b₅ is onto & b₆ is currying & b₆ is one-to-one & b₆ is onto ) ) iff for b₂ being non empty TopSpace
for b₃ being Scott complete continuous TopLattice
for b₄ being Scott TopAugmentation of ContMaps b₁,b₃ ex b₅ being Function of (ContMaps b₂,b₄),(ContMaps [:b₂,b₁:],b₃)ex b₆ being Function of (ContMaps [:b₂,b₁:],b₃),(ContMaps b₂,b₄) st
( b₅ is uncurrying & b₅ is isomorphic & b₆ is currying & b₆ is isomorphic ) ) by Lemma18;

theorem Th29: :: WAYBEL29:29

for b₁ being T_0-TopSpace holds
( InclPoset the topology of b₁ is continuous iff for b₂ being non empty TopSpace holds Theta b₂,b₁ is isomorphic )

proof end;

theorem Th30: :: WAYBEL29:30

for b₁ being T_0-TopSpace holds
( InclPoset the topology of b₁ is continuous iff for b₂ being non empty TopSpace
for b₃ being continuous Function of b₂,(Sigma (InclPoset the topology of b₁)) holds *graph b₃ is open Subset of [:b₂,b₁:] )

proof end;

theorem Th31: :: WAYBEL29:31

for b₁ being T_0-TopSpace holds
( InclPoset the topology of b₁ is continuous iff { [b₂,b₃] where B is open Subset of b₁, B is Element of b₁ : b₃ in b₂ } is open Subset of [:(Sigma (InclPoset the topology of b₁)),b₁:] )

proof end;

theorem Th32: :: WAYBEL29:32

for b₁ being T_0-TopSpace holds
( InclPoset the topology of b₁ is continuous iff for b₂ being Element of b₁
for b₃ being open a_neighborhood of b₂ ex b₄ being open Subset of (Sigma (InclPoset the topology of b₁)) st
( b₃ in b₄ & meet b₄ is a_neighborhood of b₂ ) )

proof end;

defpred S₇[ complete LATTICE] means InclPoset (sigma a₁) is continuous;

defpred S₈[ complete LATTICE] means for b₁ being Scott TopAugmentation of a₁
for b₂ being complete LATTICE
for b₃ being Scott TopAugmentation of b₂ holds sigma [:b₂,a₁:] = the topology of [:b₃,b₁:];

defpred S₉[ complete LATTICE] means for b₁ being Scott TopAugmentation of a₁
for b₂ being complete LATTICE
for b₃ being Scott TopAugmentation of b₂
for b₄ being Scott TopAugmentation of [:b₂,a₁:] holds TopStruct(# the carrier of b₄,the topology of b₄ #) = [:b₃,b₁:];

Lemma29: for b₁ being complete LATTICE holds
( S₈[b₁] iff S₉[b₁] )

proof end;

theorem Th33: :: WAYBEL29:33

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of b₁,b₃ st b₄ is isomorphic holds
for b₅ being Function of b₂,b₃ st b₅ = b₄ & b₅ is isomorphic holds
RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #)

proof end;

Lemma30: for b₁ being complete LATTICE st S₇[b₁] holds
S₈[b₁]

proof end;

Lemma31: for b₁ being complete LATTICE st S₈[b₁] holds
S₇[b₁]

proof end;

theorem Th34: :: WAYBEL29:34

for b₁ being complete LATTICE holds
( InclPoset (sigma b₁) is continuous iff for b₂ being complete LATTICE holds sigma [:b₂,b₁:] = the topology of [:(Sigma b₂),(Sigma b₁):] )

proof end;

theorem Th35: :: WAYBEL29:35

for b₁ being complete LATTICE holds
( ( for b₂ being complete LATTICE holds sigma [:b₂,b₁:] = the topology of [:(Sigma b₂),(Sigma b₁):] ) iff for b₂ being complete LATTICE holds TopStruct(# the carrier of (Sigma [:b₂,b₁:]),the topology of (Sigma [:b₂,b₁:]) #) = [:(Sigma b₂),(Sigma b₁):] )

proof end;

theorem Th36: :: WAYBEL29:36

for b₁ being complete LATTICE holds
( ( for b₂ being complete LATTICE holds sigma [:b₂,b₁:] = the topology of [:(Sigma b₂),(Sigma b₁):] ) iff for b₂ being complete LATTICE holds Sigma [:b₂,b₁:] = Omega [:(Sigma b₂),(Sigma b₁):] )

proof end;

theorem Th37: :: WAYBEL29:37

for b₁ being complete LATTICE holds
( InclPoset (sigma b₁) is continuous iff for b₂ being complete LATTICE holds Sigma [:b₂,b₁:] = Omega [:(Sigma b₂),(Sigma b₁):] )

proof end;