:: by Artur Korni{\l}owicz and Jaros{\l}aw Gryko

::

:: Received July 3, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

registration
end;

registration

for b_{1} being TopLattice st b_{1} is complete & b_{1} is Scott holds

b_{1} is T_0
by WAYBEL11:10;

end;

cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott -> T_0 for TopRelStr ;

coherence for b

b

registration
end;

registration

ex b_{1} being TopLattice st

( b_{1} is complete & b_{1} is Scott & b_{1} is strict )
end;

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ;

existence ex b

( b

proof end;

theorem Th3: :: WAYBEL25:3

for I being non empty set

for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space))

for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) 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 being_homeomorphism

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 being_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

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 :: 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 by Th5, Th6;

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 by Th5, Th6;

definition

let X, Y be non empty TopSpace;

( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X )

end;
redefine pred X is_Retract_of Y means :: 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 ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X;

( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X )

proof end;

:: deftheorem defines is_Retract_of WAYBEL25:def 1 :

for X, Y being non empty TopSpace holds

( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X );

for X, Y being non empty TopSpace holds

( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X );

theorem :: 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

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

S2 is_Retract_of T

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

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

J is_Retract_of Y

proof end;

registration

let L be complete continuous LATTICE;

coherence

for b_{1} being TopAugmentation of L st b_{1} is Scott holds

b_{1} is injective
by Th12;

end;
coherence

for b

b

registration

let T be non empty injective TopSpace;

coherence

TopStruct(# the carrier of T, the topology of T #) is injective by WAYBEL18:16;

end;
coherence

TopStruct(# the carrier of T, the topology of T #) is injective by WAYBEL18:16;

::p.124 definition 3.6

definition

let T be TopStruct ;

ex b_{1} being strict TopRelStr st

( TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b_{1} holds

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) )

for b_{1}, b_{2} being strict TopRelStr st TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b_{1} holds

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b_{2} holds

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) holds

b_{1} = b_{2}

end;
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 ( 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 ) ) ) );

ex b

( TopStruct(# the carrier of b

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) )

proof end;

uniqueness for b

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of b

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Omega WAYBEL25:def 2 :

for T being TopStruct

for b_{2} being strict TopRelStr holds

( b_{2} = Omega T iff ( TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b_{2} holds

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) ) );

for T being TopStruct

for b

( b

( x <= y iff ex Y being Subset of T st

( Y = {y} & x in Cl Y ) ) ) ) );

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

proof end;

registration
end;

Lm2: 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;

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

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))) #)

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;

::p.124 theorem 3.8 (i, part b)

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;

::p.124 theorem 3.8 (i, part b)

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 #)

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;

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

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 being_homeomorphism holds

g is isomorphic

for h being Function of S,T

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

g is isomorphic

proof end;

Lm3: 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

by WAYBEL_9:1;

::p.124 proposition 3.7

::p.124 theorem 3.8 (ii, part a)

::p.124 theorem 3.8 (ii, part a)

registration
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

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

proof end;

registration

let X, Y be non empty TopSpace;

for b_{1} being Function of (Omega X),(Omega Y) st b_{1} is continuous holds

b_{1} is monotone
by Th21;

end;
cluster Function-like quasi_total continuous -> monotone for Element of bool [: the carrier of (Omega X), the carrier of (Omega Y):];

coherence for b

b

registration

let T be non empty TopSpace;

let x be Element of (Omega T);

coherence

( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed )

downarrow x is closed

end;
let x be Element of (Omega T);

coherence

( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed )

proof end;

coherence downarrow x is closed

proof end;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of (Omega T) st b_{1} is open holds

b_{1} is upper
by Th23;

end;
coherence

for b

b

Lm4: now :: thesis: for X, Y being non empty TopSpace

for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))

for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))

let X, Y be non empty TopSpace; :: thesis: for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))

let N be net of ContMaps (X,(Omega Y)); :: thesis: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))

A1: 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)

the mapping of N in Funcs ( the carrier of N, the carrier of (ContMaps (X,(Omega Y)))) by FUNCT_2:8;

hence the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by A2; :: thesis: verum

end;
let N be net of ContMaps (X,(Omega Y)); :: thesis: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))

A1: 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

then A2:
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:56;
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in the carrier of (ContMaps (X,(Omega Y))) or f in Funcs ( the carrier of X, the carrier of Y) )

assume f in the carrier of (ContMaps (X,(Omega Y))) ; :: thesis: f in Funcs ( the carrier of X, the carrier of Y)

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 A1, FUNCT_2:8; :: thesis: verum

end;
assume f in the carrier of (ContMaps (X,(Omega Y))) ; :: thesis: f in Funcs ( the carrier of X, the carrier of Y)

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 A1, FUNCT_2:8; :: thesis: verum

the mapping of N in Funcs ( the carrier of N, the carrier of (ContMaps (X,(Omega Y)))) by FUNCT_2:8;

hence the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by A2; :: thesis: verum

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) ;

ex b_{1} being strict net of S st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{1} = (commute the mapping of N) . i )

for b_{1}, b_{2} being strict net of S st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{1} = (commute the mapping of N) . i & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{2} = (commute the mapping of N) . i holds

b_{1} = b_{2}
;

end;
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 ( 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 );

ex b

( RelStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines commute WAYBEL25:def 3 :

for I being non empty set

for S, T being non empty RelStr

for N being net of T

for i being Element of I st the carrier of T c= the carrier of (S |^ I) holds

for b_{6} being strict net of S holds

( b_{6} = commute (N,i,S) iff ( RelStr(# the carrier of b_{6}, the InternalRel of b_{6} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{6} = (commute the mapping of N) . i ) );

for I being non empty set

for S, T being non empty RelStr

for N being net of T

for i being Element of I st the carrier of T c= the carrier of (S |^ I) holds

for b

( b

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

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

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;

coherence

commute (N,x,(Omega Y)) is eventually-directed by Th25;

end;
let N be eventually-directed net of ContMaps (X,(Omega Y));

let x be Point of X;

coherence

commute (N,x,(Omega Y)) is eventually-directed by Th25;

registration

let X, Y be non empty TopSpace;

coherence

for b_{1} being net of ContMaps (X,(Omega Y)) holds b_{1} is Function-yielding
;

end;
coherence

for b

Lm5: now :: thesis: for X, Y being non empty TopSpace

for N being net of ContMaps (X,(Omega Y))

for i being Element of N holds

( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

for N being net of ContMaps (X,(Omega Y))

for i being Element of N holds

( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

let X, Y be non empty TopSpace; :: thesis: for N being net of ContMaps (X,(Omega Y))

for i being Element of N holds

( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

let N be net of ContMaps (X,(Omega Y)); :: thesis: for i being Element of N holds

( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

let i be Element of N; :: thesis: ( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

thus the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21; :: thesis: the mapping of N . i is Function of X,Y

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: verum

end;
for i being Element of N holds

( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

let N be net of ContMaps (X,(Omega Y)); :: thesis: for i being Element of N holds

( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

let i be Element of N; :: thesis: ( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )

thus the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21; :: thesis: the mapping of N . i is Function of X,Y

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: verum

Lm6: now :: thesis: for X, Y being non empty TopSpace

for N being net of ContMaps (X,(Omega Y))

for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

for N being net of ContMaps (X,(Omega Y))

for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

let X, Y be non empty TopSpace; :: thesis: for N being net of ContMaps (X,(Omega Y))

for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

let N be net of ContMaps (X,(Omega Y)); :: thesis: for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

let x be Point of X; :: thesis: dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

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: verum

end;
for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

let N be net of ContMaps (X,(Omega Y)); :: thesis: for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

let x be Point of X; :: thesis: dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))

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: verum

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

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;

::p.125 definition 3.9

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

for T being non empty TopSpace holds

( T is monotone-convergence iff 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 ) ) );

for T being non empty TopSpace holds

( T is monotone-convergence iff 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 ) ) );

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

T is monotone-convergence

proof end;

Lm7: now :: thesis: for T being non empty 1-sorted

for D being non empty Subset of T

for d being Element of T st the carrier of T = {d} holds

D = {d}

for D being non empty Subset of T

for d being Element of T st the carrier of T = {d} holds

D = {d}

let T be non empty 1-sorted ; :: thesis: for D being non empty Subset of T

for d being Element of T st the carrier of T = {d} holds

D = {d}

let D be non empty Subset of T; :: thesis: for d being Element of T st the carrier of T = {d} holds

D = {d}

let d be Element of T; :: thesis: ( the carrier of T = {d} implies D = {d} )

assume A1: the carrier of T = {d} ; :: thesis: D = {d}

thus D = {d} :: thesis: verum

end;
for d being Element of T st the carrier of T = {d} holds

D = {d}

let D be non empty Subset of T; :: thesis: for d being Element of T st the carrier of T = {d} holds

D = {d}

let d be Element of T; :: thesis: ( the carrier of T = {d} implies D = {d} )

assume A1: the carrier of T = {d} ; :: thesis: D = {d}

thus D = {d} :: thesis: verum

proof

thus
D c= {d}
by A1; :: according to XBOOLE_0:def 10 :: thesis: {d} c= D

set x = the Element of D;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {d} or a in D )

assume a in {d} ; :: thesis: a in D

then A2: a = d by TARSKI:def 1;

the Element of D in D ;

hence a in D by A1, A2, TARSKI:def 1; :: thesis: verum

end;
set x = the Element of D;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {d} or a in D )

assume a in {d} ; :: thesis: a in D

then A2: a = d by TARSKI:def 1;

the Element of D in D ;

hence a in D by A1, A2, TARSKI:def 1; :: thesis: verum

registration

coherence

for b_{1} being T_0-TopSpace st b_{1} is trivial holds

b_{1} is monotone-convergence

end;
for b

b

proof 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

for T being T_0-TopSpace st S,T are_homeomorphic holds

T is monotone-convergence

proof end;

registration

let L be complete LATTICE;

coherence

for b_{1} being Scott TopAugmentation of L holds b_{1} is monotone-convergence
by Th29;

end;
coherence

for b

registration

let L be complete LATTICE;

let S be Scott TopAugmentation of L;

coherence

TopStruct(# the carrier of S, the topology of S #) is monotone-convergence by Th27;

end;
let S be Scott TopAugmentation of L;

coherence

TopStruct(# the carrier of S, the topology of S #) is monotone-convergence by Th27;

registration
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

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

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

for N being eventually-directed net of Omega X holds N is convergent

proof end;

registration

let X be non empty monotone-convergence TopSpace;

for b_{1} being eventually-directed net of Omega X holds b_{1} is convergent
by Th33;

end;
cluster non empty transitive directed eventually-directed -> eventually-directed convergent for NetStr over Omega X;

coherence for b

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

( ex_sup_of N & sup N in Lim N ) ) holds

X is monotone-convergence

proof end;

::p.125 lemma 3.10

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

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;

for b_{1} being Function of (Omega X),(Omega Y) st b_{1} is continuous holds

b_{1} is directed-sups-preserving
by Th35;

end;
let Y be T_0-TopSpace;

cluster Function-like quasi_total continuous -> directed-sups-preserving for Element of bool [: the carrier of (Omega X), the carrier of (Omega Y):];

coherence for b

b

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

for R being T_0-TopSpace st R is_Retract_of T holds

R is monotone-convergence

proof end;

::p.124 theorem 3.8 (ii, part b)

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 #)

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;

registration

coherence

for b_{1} being T_0-TopSpace st b_{1} is injective holds

b_{1} is monotone-convergence
by Th39;

end;
for b

b

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

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)))

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;

::p.125 lemma 3.11

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

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;

::p.126 lemma 3.12 (i)

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

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;

:: p.124 theorem 3.8 (i, part a)

:: p.126 exercise 3.14