:: WAYBEL25 semantic presentation

theorem :: WAYBEL25:1

for p being Point of Sierpinski_Space st p = 0 holds
{p} is closed

proof end;

theorem Th2: :: WAYBEL25:2

for p being Point of Sierpinski_Space st p = 1 holds
not {p} is closed

proof end;

registration

cluster Sierpinski_Space -> non being_T1 ;
coherence

proof end;

end;

registration

cluster complete Scott -> discerning TopRelStr ;
coherence by WAYBEL11:10;

end;

registration

cluster strict injective TopStruct ;
existence

proof end;

end;

registration

cluster discerning complete strict Scott TopRelStr ;
existence

proof end;

end;

theorem Th3: :: WAYBEL25:3

for I being non empty set
for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space ))

proof end;

theorem Th4: :: WAYBEL25:4

for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2
for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is_homeomorphism

proof end;

theorem Th5: :: WAYBEL25:5

for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic

proof end;

theorem Th6: :: WAYBEL25:6

for S, T being non empty TopSpace st S is injective & S,T are_homeomorphic holds
T is injective

proof end;

theorem :: WAYBEL25:7

for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic & T1 is injective holds
T2 is injective

proof end;

definition

let X, Y be non empty TopSpace;
redefine pred X is_Retract_of Y means :Def1: :: WAYBEL25:def 1
ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X;
compatibility

proof end;

end;

:: deftheorem Def1 defines is_Retract_of WAYBEL25:def 1 :

theorem Th8: :: WAYBEL25:8

for S, T, X, Y being non empty TopSpace st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #) & S is_Retract_of X holds
T is_Retract_of Y

proof end;

theorem :: WAYBEL25:9

for T, S1, S2 being non empty TopStruct st S1,S2 are_homeomorphic & S1 is_Retract_of T holds
S2 is_Retract_of T

proof end;

theorem :: WAYBEL25:10

for S, T being non empty TopSpace st T is injective & S is_Retract_of T holds
S is injective

proof end;

theorem :: WAYBEL25:11

for J being non empty injective TopSpace
for Y being non empty TopSpace st J is SubSpace of Y holds
J is_Retract_of Y

proof end;

theorem Th12: :: WAYBEL25:12

for L being complete continuous LATTICE
for T being Scott TopAugmentation of L holds T is injective

proof end;

registration

let L be complete continuous LATTICE;
cluster Scott -> injective TopAugmentation of L;
coherence by Th12;

end;

registration

let T be non empty injective TopSpace;
cluster TopStruct(# the carrier of T,the topology of T #) -> injective ;
coherence by WAYBEL18:17;

end;

definition

let T be TopStruct ;
func Omega T -> strict TopRelStr means :Def2: :: WAYBEL25:def 2
( TopStruct(# the carrier of it,the topology of it #) = TopStruct(# the carrier of T,the topology of T #) & ( for x, y being Element of it holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Omega WAYBEL25:def 2 :

Lm1: for T being TopStruct holds the carrier of T = the carrier of (Omega T)

proof end;

then Lm2: for T being TopStruct
for a being set holds
( a is Subset of T iff a is Subset of (Omega T) )
;

registration

let T be empty TopStruct ;
cluster Omega T -> empty strict ;
coherence

proof end;

end;

registration

let T be non empty TopStruct ;
cluster Omega T -> non empty strict ;
coherence

proof end;

end;

registration

let T be TopSpace;
cluster Omega T -> TopSpace-like strict ;
coherence

proof end;

end;

registration

let T be TopStruct ;
cluster Omega T -> reflexive strict ;
coherence

proof end;

end;

Lm3: for T being TopStruct
for x, y being Element of T
for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )

proof end;

registration

let T be TopStruct ;
cluster Omega T -> reflexive transitive strict ;
coherence

proof end;

end;

registration

let T be T_0-TopSpace;
cluster Omega T -> non empty TopSpace-like reflexive transitive antisymmetric strict ;
coherence

proof end;

end;

theorem Th13: :: WAYBEL25:13

for S, T being TopSpace st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
Omega S = Omega T

proof end;

theorem :: WAYBEL25:14

for M being non empty set
for T being non empty TopSpace holds RelStr(# the carrier of (Omega (product (M --> T))),the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))),the InternalRel of (product (M --> (Omega T))) #)

proof end;

theorem Th15: :: WAYBEL25:15

for S being complete Scott TopLattice holds Omega S = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #)

proof end;

theorem Th16: :: WAYBEL25:16

for L being complete LATTICE
for S being Scott TopAugmentation of L holds RelStr(# the carrier of (Omega S),the InternalRel of (Omega S) #) = RelStr(# the carrier of L,the InternalRel of L #)

proof end;

registration

let S be complete Scott TopLattice;
cluster Omega S -> non empty TopSpace-like reflexive transitive antisymmetric complete strict ;
coherence

proof end;

end;

theorem Th17: :: WAYBEL25:17

for T being non empty TopSpace
for S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T

proof end;

theorem Th18: :: WAYBEL25:18

for S, T being TopSpace
for h being Function of S,T
for g being Function of (Omega S),(Omega T) st h = g & h is_homeomorphism holds
g is isomorphic

proof end;

theorem Th19: :: WAYBEL25:19

for S, T being TopSpace st S,T are_homeomorphic holds
Omega S, Omega T are_isomorphic

proof end;

Lm4: for S, T being non empty RelStr
for f being Function of S,S
for g being Function of T,T st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & f = g & f is projection holds
g is projection

proof end;

theorem Th20: :: WAYBEL25:20

for T being injective T_0-TopSpace holds Omega T is complete continuous LATTICE

proof end;

registration

let T be injective T_0-TopSpace;
cluster Omega T -> non empty TopSpace-like reflexive transitive antisymmetric complete strict continuous ;
coherence by Th20;

end;

theorem Th21: :: WAYBEL25:21

for X, Y being non empty TopSpace
for f being continuous Function of (Omega X),(Omega Y) holds f is monotone

proof end;

registration

let X, Y be non empty TopSpace;
cluster continuous -> monotone Relation of the carrier of (Omega X),the carrier of (Omega Y);
coherence by Th21;

end;

theorem Th22: :: WAYBEL25:22

for T being non empty TopSpace
for x being Element of (Omega T) holds Cl {x} = downarrow x

proof end;

registration

let T be non empty TopSpace;
let x be Element of (Omega T);
cluster Cl {x} -> non empty directed lower ;
coherence

proof end;

cluster downarrow x -> closed ;
coherence

proof end;

end;

theorem Th23: :: WAYBEL25:23

for X being TopSpace
for A being open Subset of (Omega X) holds A is upper

proof end;

registration

let T be TopSpace;
cluster open -> upper Element of bool the carrier of (Omega T);
coherence by Th23;

end;

Lm5: now

let X, Y be non empty TopSpace; :: thesis:
let N be net of ContMaps X,(Omega Y); :: thesis:
A1: the mapping of N in Funcs the carrier of N,the carrier of (ContMaps X,(Omega Y)) by FUNCT_2:11;
A2: the carrier of Y = the carrier of (Omega Y) by Lm1;
the carrier of (ContMaps X,(Omega Y)) c= Funcs the carrier of X,the carrier of Y

proof

let f be set ; :: according to TARSKI:def 3 :: thesis:
assume f in the carrier of (ContMaps X,(Omega Y)) ; :: thesis:
then ex x being Function of X,(Omega Y) st
( x = f & x is continuous ) by WAYBEL24:def 3;
hence f in Funcs the carrier of X,the carrier of Y by A2, FUNCT_2:11; :: thesis:

end;

then Funcs the carrier of N,the carrier of (ContMaps X,(Omega Y)) c= Funcs the carrier of N,(Funcs the carrier of X,the carrier of Y) by FUNCT_5:63;
hence the mapping of N in Funcs the carrier of N,(Funcs the carrier of X,the carrier of Y) by A1; :: thesis:

end;

definition

let I be non empty set ;
let S, T be non empty RelStr ;
let N be net of T;
let i be Element of I;
assume A1: the carrier of T c= the carrier of (S |^ I) ;
func commute N,i,S -> strict net of S means :Def3: :: WAYBEL25:def 3
( RelStr(# the carrier of it,the InternalRel of it #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of it = (commute the mapping of N) . i );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines commute WAYBEL25:def 3 :

theorem Th24: :: WAYBEL25:24

for X, Y being non empty TopSpace
for N being net of ContMaps X,(Omega Y)
for i being Element of N
for x being Point of X holds the mapping of (commute N,x,(Omega Y)) . i = (the mapping of N . i) . x

proof end;

theorem Th25: :: WAYBEL25:25

for X, Y being non empty TopSpace
for N being eventually-directed net of ContMaps X,(Omega Y)
for x being Point of X holds commute N,x,(Omega Y) is eventually-directed

proof end;

registration

let X, Y be non empty TopSpace;
let N be eventually-directed net of ContMaps X,(Omega Y);
let x be Point of X;
cluster commute N,x,(Omega Y) -> strict eventually-directed ;
coherence by Th25;

end;

registration

let X, Y be non empty TopSpace;
cluster -> Function-yielding NetStr of ContMaps X,(Omega Y);
coherence ;

end;

Lm6: now

let X, Y be non empty TopSpace; :: thesis:
let N be net of ContMaps X,(Omega Y); :: thesis:
let i be Element of N; :: thesis:
thus the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21; :: thesis:
the carrier of Y = the carrier of (Omega Y) by Lm1;
hence the mapping of N . i is Function of X,Y by WAYBEL24:21; :: thesis:

end;

Lm7: now

let X, Y be non empty TopSpace; :: thesis:
let N be net of ContMaps X,(Omega Y); :: thesis:
let x be Point of X; :: thesis:
ContMaps X,(Omega Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;
then the carrier of (ContMaps X,(Omega Y)) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def 13;
then A1: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of (commute N,x,(Omega Y)),the InternalRel of (commute N,x,(Omega Y)) #) by Def3;
thus dom the mapping of N = the carrier of N by FUNCT_2:def 1
.= dom the mapping of (commute N,x,(Omega Y)) by A1, FUNCT_2:def 1 ; :: thesis:

end;

theorem Th26: :: WAYBEL25:26

for X being non empty TopSpace
for Y being T_0-TopSpace
for N being net of ContMaps X,(Omega Y) st ( for x being Point of X holds ex_sup_of commute N,x,(Omega Y) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X

proof end;

definition

let T be non empty TopSpace;
attr T is monotone-convergence means :Def4: :: WAYBEL25:def 4
for D being non empty directed Subset of (Omega T) holds
( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) );

end;

:: deftheorem Def4 defines monotone-convergence WAYBEL25:def 4 :

theorem Th27: :: WAYBEL25:27

for S, T being non empty TopSpace st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is monotone-convergence holds
T is monotone-convergence

proof end;

Lm8: now

let T be non empty 1-sorted ; :: thesis:
let D be non empty Subset of T; :: thesis:
let d be Element of T; :: thesis:
assume A1: the carrier of T = {d} ; :: thesis:
thus D = {d} :: thesis:

proof

thus D c= {d} by A1; :: according to XBOOLE_0:def 10 :: thesis:
let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {d} ; :: thesis:
then A2: a = d by TARSKI:def 1;
consider x being Element of D;
x in D ;
hence a in D by A1, A2, TARSKI:def 1; :: thesis:

end;

registration

cluster trivial -> monotone-convergence TopStruct ;
coherence

proof end;

end;

registration

cluster non empty strict trivial monotone-convergence TopStruct ;
existence

proof end;

end;

theorem :: WAYBEL25:28

for S being monotone-convergence T_0-TopSpace
for T being T_0-TopSpace st S,T are_homeomorphic holds
T is monotone-convergence

proof end;

theorem Th29: :: WAYBEL25:29

for S being complete Scott TopLattice holds S is monotone-convergence

proof end;

registration

let L be complete LATTICE;
cluster Scott -> discerning Scott monotone-convergence TopAugmentation of L;
coherence by Th29;

end;

registration

let L be complete LATTICE;
let S be Scott TopAugmentation of L;
cluster TopStruct(# the carrier of S,the topology of S #) -> monotone-convergence ;
coherence by Th27;

end;

theorem Th30: :: WAYBEL25:30

for X being monotone-convergence T_0-TopSpace holds Omega X is up-complete

proof end;

registration

let X be monotone-convergence T_0-TopSpace;
cluster Omega X -> non empty TopSpace-like reflexive transitive antisymmetric up-complete strict ;
coherence by Th30;

end;

theorem Th31: :: WAYBEL25:31

for X being non empty monotone-convergence TopSpace
for N being eventually-directed prenet of Omega X holds ex_sup_of N

proof end;

theorem Th32: :: WAYBEL25:32

for X being non empty monotone-convergence TopSpace
for N being eventually-directed net of Omega X holds sup N in Lim N

proof end;

theorem Th33: :: WAYBEL25:33

for X being non empty monotone-convergence TopSpace
for N being eventually-directed net of Omega X holds N is convergent

proof end;

registration

let X be non empty monotone-convergence TopSpace;
cluster eventually-directed -> eventually-directed convergent NetStr of Omega X;
coherence by Th33;

end;

theorem :: WAYBEL25:34

for X being non empty TopSpace st ( for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ) holds
X is monotone-convergence

proof end;

theorem Th35: :: WAYBEL25:35

for X being non empty monotone-convergence TopSpace
for Y being T_0-TopSpace
for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving

proof end;

registration

let X be non empty monotone-convergence TopSpace;
let Y be T_0-TopSpace;
cluster continuous -> directed-sups-preserving Relation of the carrier of (Omega X),the carrier of (Omega Y);
coherence by Th35;

end;

theorem Th36: :: WAYBEL25:36

for T being monotone-convergence T_0-TopSpace
for R being T_0-TopSpace st R is_Retract_of T holds
R is monotone-convergence

proof end;

theorem Th37: :: WAYBEL25:37

for T being injective T_0-TopSpace
for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #)

proof end;

theorem :: WAYBEL25:38

for T being injective T_0-TopSpace holds
( T is compact & T is locally-compact & T is sober )

proof end;

theorem Th39: :: WAYBEL25:39

for T being injective T_0-TopSpace holds T is monotone-convergence

proof end;

registration

cluster injective -> monotone-convergence TopStruct ;
coherence by Th39;

end;

theorem Th40: :: WAYBEL25:40

for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps X,(Omega Y)
for f, g being Function of X,(Omega Y) st f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f

proof end;

theorem Th41: :: WAYBEL25:41

for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps X,(Omega Y)
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute N,a,(Omega Y) is eventually-directed ) & f = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) holds
f . x = sup (commute N,x,(Omega Y))

proof end;

theorem Th42: :: WAYBEL25:42

for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps X,(Omega Y) st ( for x being Point of X holds commute N,x,(Omega Y) is eventually-directed ) holds
"\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) is continuous Function of X,Y

proof end;

theorem :: WAYBEL25:43

for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace holds ContMaps X,(Omega Y) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X

proof end;