:: WAYBEL29 semantic presentation

for S, T being non empty 1-sorted
for f being Function of S,T st f is one-to-one & f is onto holds
( f * (f " ) = id T & (f " ) * f = id S & f " is one-to-one & f " is onto )

proof end;

theorem Th2: :: WAYBEL29:2

for X, Y being non empty set
for Z being non empty RelStr
for S being non empty SubRelStr of Z |^ [:X,Y:]
for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is one-to-one & f is onto holds
f " is uncurrying

proof end;

theorem Th3: :: WAYBEL29:3

for X, Y being non empty set
for Z being non empty RelStr
for S being non empty SubRelStr of Z |^ [:X,Y:]
for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of T,S st f is uncurrying & f is one-to-one & f is onto holds
f " is currying

proof end;

theorem :: WAYBEL29:4

for X, Y being non empty set
for Z being non empty Poset
for S being non empty full SubRelStr of Z |^ [:X,Y:]
for T being non empty full SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is one-to-one & f is onto holds
f is isomorphic

proof end;

theorem :: WAYBEL29:5

for X, Y being non empty set
for Z being non empty Poset
for T being non empty full SubRelStr of Z |^ [:X,Y:]
for S being non empty full SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is uncurrying & f is one-to-one & f is onto holds
f is isomorphic

proof end;

theorem Th6: :: WAYBEL29:6

for S1, S2, T1, T2 being RelStr st RelStr(# the carrier of S1,the InternalRel of S1 #) = RelStr(# the carrier of S2,the InternalRel of S2 #) & RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) holds
for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic

proof end;

theorem Th7: :: WAYBEL29:7

for R, S, T being RelStr
for f being Function of R,S st f is isomorphic holds
for g being Function of S,T st g is isomorphic holds
for h being Function of R,T st h = g * f holds
h is isomorphic

proof end;

theorem :: WAYBEL29:8

canceled;

theorem :: WAYBEL29:9

canceled;

theorem Th10: :: WAYBEL29:10

for X, Y, X1, Y1 being TopSpace st TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of X1,the topology of X1 #) & TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of Y1,the topology of Y1 #) holds
[:X,Y:] = [:X1,Y1:]

proof end;

theorem Th11: :: WAYBEL29:11

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

proof end;

theorem Th12: :: WAYBEL29:12

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

proof end;

theorem Th13: :: WAYBEL29:13

for S1, S2 being TopStruct st TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) holds
for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1,the InternalRel of T1,the topology of T1 #) = TopRelStr(# the carrier of T2,the InternalRel of T2,the topology of T2 #) holds
ContMaps S1,T1 = ContMaps S2,T2

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 X be non empty TopSpace;
let L be non empty up-complete Scott TopPoset;
cluster ContMaps X,L -> up-complete ;
coherence

proof end;

end;

theorem Th14: :: WAYBEL29:14

for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds
I -POS_prod J is up-complete

proof end;

theorem :: WAYBEL29:15

for I being non empty set
for J being non-Empty reflexive-yielding Poset-yielding ManySortedSet of I st ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) holds
for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )

proof end;

registration

let X be set ;
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster L |^ X -> lower-bounded ;
coherence

proof end;

end;

registration

let X be non empty TopSpace;
let L be non empty lower-bounded TopPoset;
cluster ContMaps X,L -> lower-bounded ;
coherence

proof end;

end;

registration

let L be non empty up-complete Poset;
cluster -> up-complete TopAugmentation of L;
coherence

proof end;

cluster Scott -> correct TopAugmentation of L;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem :: WAYBEL29:16

canceled;

theorem Th17: :: WAYBEL29:17

for L being non empty up-complete Poset
for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2

proof end;

theorem Th18: :: WAYBEL29:18

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

proof end;

definition

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

proof end;

existence ;

end;

:: deftheorem Def1 defines Sigma WAYBEL29:def 1 :

theorem Th19: :: WAYBEL29:19

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

proof end;

theorem Th20: :: WAYBEL29:20

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

proof end;

definition

let S, T be non empty up-complete Poset;
let f be Function of S,T;
func Sigma f -> Function of (Sigma S),(Sigma T) equals :: WAYBEL29:def 2
f;
coherence

proof end;

end;

:: deftheorem defines Sigma WAYBEL29:def 2 :

registration

let S, T be non empty up-complete Poset;
let f be directed-sups-preserving Function of S,T;
cluster Sigma f -> continuous ;
coherence

proof end;

end;

theorem :: WAYBEL29:21

for S, T being non empty up-complete Poset
for f being Function of S,T holds
( f is isomorphic iff Sigma f is isomorphic )

proof end;

theorem Th22: :: WAYBEL29:22

for X being non empty TopSpace
for S being Scott complete TopLattice holds oContMaps X,S = ContMaps X,S

proof end;

definition

let X, Y be non empty TopSpace;
func Theta X,Y -> Function of (InclPoset the topology of [:X,Y:]),(ContMaps X,(Sigma (InclPoset the topology of Y))) means :Def3: :: WAYBEL29:def 3
for W being open Subset of [:X,Y:] holds it . W = W,the carrier of X *graph ;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines Theta WAYBEL29:def 3 :

defpred S₁[ T_0-TopSpace] means for X being non empty TopSpace
for L being Scott complete continuous TopLattice
for T being Scott TopAugmentation of ContMaps $1,L ex f being Function of (ContMaps X,T),(ContMaps [:X,$1:],L) ex g being Function of (ContMaps [:X,$1:],L),(ContMaps X,T) st
( f is uncurrying & f is one-to-one & f is onto & g is currying & g is one-to-one & g is onto );

defpred S₂[ T_0-TopSpace] means for X being non empty TopSpace
for L being Scott complete continuous TopLattice
for T being Scott TopAugmentation of ContMaps $1,L ex f being Function of (ContMaps X,T),(ContMaps [:X,$1:],L) ex g being Function of (ContMaps [:X,$1:],L),(ContMaps X,T) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic );

defpred S₃[ T_0-TopSpace] means for X being non empty TopSpace holds Theta X,$1 is isomorphic;

defpred S₄[ T_0-TopSpace] means for X being non empty TopSpace
for T being Scott TopAugmentation of InclPoset the topology of $1
for f being continuous Function of X,T holds *graph f is open Subset of [:X,$1:];

defpred S₅[ T_0-TopSpace] means for T being Scott TopAugmentation of InclPoset the topology of $1 holds { [W,y] where W is open Subset of $1, y is Element of $1 : y in W } is open Subset of [:T,$1:];

defpred S₆[ T_0-TopSpace] means for S being Scott TopAugmentation of InclPoset the topology of $1
for y being Element of $1
for V being open a_neighborhood of y ex H being open Subset of S st
( V in H & meet H is a_neighborhood of y );

Lm1: for T being T_0-TopSpace holds
( S₁[T] iff S₂[T] )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines alpha WAYBEL29:def 4 :

theorem :: WAYBEL29:23

for X being non empty TopSpace
for V being open Subset of X holds ((alpha X) " ) . V = chi V,the carrier of X

proof end;

registration

let X be non empty TopSpace;
cluster alpha X -> isomorphic ;
coherence

proof end;

end;

registration

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

end;

registration

let S be injective T_0-TopSpace;
cluster Omega S -> Scott injective T_0 ;
coherence

proof end;

end;

registration

let X be non empty TopSpace;
cluster oContMaps X,Sierpinski_Space -> complete ;
coherence

proof end;

end;

theorem :: WAYBEL29:24

Omega Sierpinski_Space = Sigma (BoolePoset 1)

proof end;

registration

let M be non empty set ;
let S be injective T_0-TopSpace;
cluster product (M => S) -> injective ;
coherence

proof end;

end;

theorem :: WAYBEL29:25

for M being non empty set
for L being complete continuous LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))

proof end;

theorem :: WAYBEL29:26

for M being non empty set
for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))

proof end;

definition

let M be non empty set ;
let X, Y be non empty TopSpace;
func commute X,M,Y -> Function of (oContMaps X,(M -TOP_prod (M => Y))),((oContMaps X,Y) |^ M) means :Def5: :: WAYBEL29:def 5
for f being continuous Function of X,(M -TOP_prod (M => Y)) holds it . f = commute f;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def5 defines commute WAYBEL29:def 5 :

registration

let M be non empty set ;
let X, Y be non empty TopSpace;
cluster commute X,M,Y -> V5 onto ;
correctness

proof end;

end;

registration

let M be non empty set ;
let X be non empty TopSpace;
cluster commute X,M,Sierpinski_Space -> V5 onto isomorphic ;
correctness

proof end;

end;

Lm2: for T being T_0-TopSpace st S₃[T] holds
S₄[T]

proof end;

theorem Th27: :: WAYBEL29:27

for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for f1, f2 being Element of (ContMaps X,S) st f1 <= f2 holds
*graph f1 c= *graph f2

proof end;

Lm3: for T being T_0-TopSpace st S₄[T] holds
S₃[T]

proof end;

Lm4: for T being T_0-TopSpace st S₄[T] holds
S₅[T]

proof end;

Lm5: for T being T_0-TopSpace st S₅[T] holds
S₆[T]

proof end;

Lm6: for T being T_0-TopSpace st S₆[T] holds
S₄[T]

proof end;

Lm7: for T being T_0-TopSpace st S₆[T] holds
InclPoset the topology of T is continuous

proof end;

Lm8: for T being T_0-TopSpace st InclPoset the topology of T is continuous holds
S₆[T]

proof end;

theorem :: WAYBEL29:28

for Y being T_0-TopSpace holds
( ( for X being non empty TopSpace
for L being Scott complete continuous TopLattice
for T being Scott TopAugmentation of ContMaps Y,L ex f being Function of (ContMaps X,T),(ContMaps [:X,Y:],L) ex g being Function of (ContMaps [:X,Y:],L),(ContMaps X,T) st
( f is uncurrying & f is one-to-one & f is onto & g is currying & g is one-to-one & g is onto ) ) iff for X being non empty TopSpace
for L being Scott complete continuous TopLattice
for T being Scott TopAugmentation of ContMaps Y,L ex f being Function of (ContMaps X,T),(ContMaps [:X,Y:],L) ex g being Function of (ContMaps [:X,Y:],L),(ContMaps X,T) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1;

theorem :: WAYBEL29:29

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

proof end;

theorem :: WAYBEL29:30

for Y being T_0-TopSpace holds
( InclPoset the topology of Y is continuous iff for X being non empty TopSpace
for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] )

proof end;

theorem :: WAYBEL29:31

for Y being T_0-TopSpace holds
( InclPoset the topology of Y is continuous iff { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] )

proof end;

theorem :: WAYBEL29:32

for Y being T_0-TopSpace holds
( InclPoset the topology of Y is continuous iff for y being Element of Y
for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st
( V in H & meet H is a_neighborhood of y ) )

proof end;

defpred S₇[ complete LATTICE] means InclPoset (sigma $1) is continuous;

defpred S₈[ complete LATTICE] means for SL being Scott TopAugmentation of $1
for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,$1:] = the topology of [:SS,SL:];

defpred S₉[ complete LATTICE] means for SL being Scott TopAugmentation of $1
for S being complete LATTICE
for SS being Scott TopAugmentation of S
for SSL being Scott TopAugmentation of [:S,$1:] holds TopStruct(# the carrier of SSL,the topology of SSL #) = [:SS,SL:];

Lm9: for L being complete LATTICE holds
( S₈[L] iff S₉[L] )

proof end;

theorem :: WAYBEL29:33

for R1, R2, R3 being non empty RelStr
for f1 being Function of R1,R3 st f1 is isomorphic holds
for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds
RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #)

proof end;

Lm10: for L being complete LATTICE st S₇[L] holds
S₈[L]

proof end;

Lm11: for L being complete LATTICE st S₈[L] holds
S₇[L]

proof end;

theorem Th34: :: WAYBEL29:34

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

proof end;

theorem Th35: :: WAYBEL29:35

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

proof end;

theorem Th36: :: WAYBEL29:36

for L being complete LATTICE holds
( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

proof end;

theorem :: WAYBEL29:37

for L being complete LATTICE holds
( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

proof end;