:: The Characterization of Continuity of Topologies
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: WAYBEL29:1
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 V7() & f is onto holds
f " is uncurrying
proofend;

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 T,S st f is uncurrying & f is V7() & f is onto holds
f " is currying
proofend;

theorem :: WAYBEL29:3
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 V7() & f is onto holds
f is isomorphic
proofend;

theorem :: WAYBEL29:4
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 V7() & f is onto holds
f is isomorphic
proofend;

theorem Th5: :: WAYBEL29:5
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
proofend;

:: Przywlaszczone
theorem Th6: :: WAYBEL29:6
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
proofend;

theorem Th7: :: WAYBEL29:7
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:]
proofend;

theorem Th8: :: WAYBEL29:8
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
proofend;

theorem Th9: :: WAYBEL29:9
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
proofend;

theorem Th10: :: WAYBEL29:10
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)
proofend;

registration
cluster TopSpace-like reflexive transitive antisymmetric Scott continuous with_suprema with_infima complete  ->  T_0 continuous injective complete for TopRelStr ;
coherence
 for b1 being continuous complete TopLattice st b1 is Scott holds
( b1 is injective & b1 is T_0 )
proofend;
end;

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric Scott continuous non void with_suprema with_infima complete for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is Scott & b1 is continuous & b1 is complete )
proofend;
end;

registration
let X be non empty TopSpace;
let L be non empty up-complete Scott TopPoset;
cluster ContMaps (X,L) ->  up-complete ;
coherence
 ContMaps (X,L) is up-complete
proofend;
end;

theorem Th11: :: WAYBEL29:11
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
proofend;

theorem :: WAYBEL29:12
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 & 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 ) &amp; 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) ) )
proofend;

registration
let X be set ;
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
clusterL |^ X ->  lower-bounded ;
coherence
 L |^ X is lower-bounded
proofend;
end;

registration
let X be non empty TopSpace;
let L be non empty lower-bounded TopPoset;
cluster ContMaps (X,L) ->  lower-bounded ;
coherence
 ContMaps (X,L) is lower-bounded
proofend;
end;

registration
let L be non empty up-complete Poset;
cluster  ->  up-complete for TopAugmentation of L;
coherence
 for b1 being TopAugmentation of L holds b1 is up-complete
proofend;
cluster Scott  ->  correct for TopAugmentation of L;
coherence
 for b1 being TopAugmentation of L st b1 is Scott holds
b1 is correct
proofend;
end;

registration
let L be non empty up-complete Poset;
cluster non empty reflexive transitive antisymmetric up-complete strict Scott non void for TopAugmentation of L;
existence
 ex b1 being TopAugmentation of L st
( b1 is strict &amp; b1 is Scott )
proofend;
end;

theorem Th13: :: WAYBEL29:13
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
proofend;

theorem Th14: :: WAYBEL29:14
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 #) &amp; S1 is Scott holds
S2 is Scott
proofend;

definition
let L be non empty up-complete Poset;
func Sigma L ->  strict Scott TopAugmentation of L means :Def1: :: WAYBEL29:def 1
verum;
uniqueness
 for b1, b2 being strict Scott TopAugmentation of L holds b1 = b2
proofend;
existence
 ex b1 being strict Scott TopAugmentation of L st verum ;
end;

:: deftheorem Def1 defines Sigma WAYBEL29:def_1_:_
 for L being non empty up-complete Poset
for b2 being strict Scott TopAugmentation of L holds
( b2 = Sigma L iff verum );

theorem Th15: :: WAYBEL29:15
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 #)
proofend;

theorem Th16: :: WAYBEL29:16
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
proofend;

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
 f is Function of (Sigma S),(Sigma T)
proofend;
end;

:: deftheorem  defines Sigma WAYBEL29:def_2_:_
 for S, T being non empty up-complete Poset
for f being Function of S,T holds Sigma f = f;

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
 Sigma f is continuous
proofend;
end;

theorem :: WAYBEL29:17
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 )
proofend;

theorem Th18: :: WAYBEL29:18
for X being non empty TopSpace
for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S)
proofend;

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
 ex b1 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st
for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph
proofend;
correctness
uniqueness
for b1, b2 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st ( for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph ) &amp; ( for W being open Subset of [:X,Y:] holds b2 . W = (W, the carrier of X) *graph ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def3 defines Theta WAYBEL29:def_3_:_
 for X, Y being non empty TopSpace
for b3 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds
( b3 = Theta (X,Y) iff for W being open Subset of [:X,Y:] holds b3 . W = (W, the carrier of X) *graph );

defpred S1[ T_0-TopSpace] means  for X being non empty TopSpace
for L being Scott continuous complete 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 &amp; f is V7() &amp; f is onto &amp; g is currying &amp; g is V7() &amp; g is onto );

defpred S2[ T_0-TopSpace] means  for X being non empty TopSpace
for L being Scott continuous complete 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 &amp; f is isomorphic &amp; g is currying &amp; g is isomorphic );

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

defpred S4[ 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 S5[ 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 S6[ 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 &amp; meet H is a_neighborhood of y );

Lm1:  for T being T_0-TopSpace holds
( S1[T] iff S2[T] )
proofend;

begin

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
 ex b1 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st
for g being continuous Function of X,Sierpinski_Space holds b1 . g = g " {1}
proofend;
uniqueness
 for b1, b2 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st ( for g being continuous Function of X,Sierpinski_Space holds b1 . g = g " {1} ) &amp; ( for g being continuous Function of X,Sierpinski_Space holds b2 . g = g " {1} ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines alpha WAYBEL29:def_4_:_
 for X being non empty TopSpace
for b2 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) holds
( b2 = alpha X iff for g being continuous Function of X,Sierpinski_Space holds b2 . g = g " {1} );

theorem :: WAYBEL29:19
for X being non empty TopSpace
for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X)
proofend;

registration
let X be non empty TopSpace;
cluster alpha X ->  isomorphic ;
coherence
 alpha X is isomorphic
proofend;
end;

registration
let X be non empty TopSpace;
cluster(alpha X) "  ->  isomorphic ;
coherence
 (alpha X) " is isomorphic by YELLOW14:10;
end;

registration
let S be injective T_0-TopSpace;
cluster Omega S ->  Scott ;
coherence
 Omega S is Scott
proofend;
end;

registration
let X be non empty TopSpace;
cluster oContMaps (X,Sierpinski_Space) ->  complete ;
coherence
 oContMaps (X,Sierpinski_Space) is complete
proofend;
end;

theorem :: WAYBEL29:20
Omega Sierpinski_Space = Sigma (BoolePoset 1)
proofend;

registration
let M be non empty set ;
let S be injective T_0-TopSpace;
cluster product (M => S) ->  injective ;
coherence
 M -TOP_prod (M => S) is injective
proofend;
end;

theorem :: WAYBEL29:21
for M being non empty set
for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))
proofend;

theorem :: WAYBEL29:22
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)))
proofend;

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
 for b1, b2 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f ) &amp; ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b2 . f = commute f ) holds
b1 = b2
proofend;
existence
 ex b1 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st
for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f
proofend;
end;

:: deftheorem Def5 defines commute WAYBEL29:def_5_:_
 for M being non empty set
for X, Y being non empty TopSpace
for b4 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) holds
( b4 = commute (X,M,Y) iff for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b4 . f = commute f );

registration
let M be non empty set ;
let X, Y be non empty TopSpace;
cluster commute (X,M,Y) -> V7() onto ;
correctness
coherence
( commute (X,M,Y) is one-to-one &amp; commute (X,M,Y) is onto );
proofend;
end;

registration
let M be non empty set ;
let X be non empty TopSpace;
cluster commute (X,M,Sierpinski_Space) ->  isomorphic ;
correctness
coherence
commute (X,M,Sierpinski_Space) is isomorphic ;
proofend;
end;

Lm2:  for T being T_0-TopSpace st S3[T] holds
S4[T]
proofend;

theorem Th23: :: WAYBEL29:23
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
proofend;

Lm3:  for T being T_0-TopSpace st S4[T] holds
S3[T]
proofend;

Lm4:  for T being T_0-TopSpace st S4[T] holds
S5[T]
proofend;

Lm5:  for T being T_0-TopSpace st S5[T] holds
S6[T]
proofend;

Lm6:  for T being T_0-TopSpace st S6[T] holds
S4[T]
proofend;

Lm7:  for T being T_0-TopSpace st S6[T] holds
InclPoset the topology of T is continuous
proofend;

Lm8:  for T being T_0-TopSpace st InclPoset the topology of T is continuous holds
S6[T]
proofend;

begin

:: 4.10. THEOREM, (1) <=> (1'), pp. 131-133
theorem :: WAYBEL29:24
for Y being T_0-TopSpace holds
( ( for X being non empty TopSpace
for L being Scott continuous complete 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 &amp; f is V7() &amp; f is onto &amp; g is currying &amp; g is V7() &amp; g is onto ) ) iff for X being non empty TopSpace
for L being Scott continuous complete 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 &amp; f is isomorphic &amp; g is currying &amp; g is isomorphic ) ) by Lm1;

:: 4.10. THEOREM, (6) <=> (2), pp. 131-133
theorem :: WAYBEL29:25
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 )
proofend;

:: 4.10. THEOREM, (6) <=> (3), pp. 131-133
theorem :: WAYBEL29:26
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:] )
proofend;

:: 4.10. THEOREM, (6) <=> (4), pp. 131-133
theorem :: WAYBEL29:27
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:] )
proofend;

:: 4.10. THEOREM, (6) <=> (5), pp. 131-133
theorem :: WAYBEL29:28
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 &amp; meet H is a_neighborhood of y ) )
proofend;

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

defpred S8[ 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 S9[ 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
( S8[L] iff S9[L] )
proofend;

begin

theorem :: WAYBEL29:29
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 &amp; f2 is isomorphic holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
proofend;

Lm10:  for L being complete LATTICE st S7[L] holds
S8[L]
proofend;

Lm11:  for L being complete LATTICE st S8[L] holds
S7[L]
proofend;

:: 4.11. THEOREM, (1) <=> (2), p. 133.
theorem Th30: :: WAYBEL29:30
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):] )
proofend;

:: 4.11. THEOREM, (2) <=> (3), p. 133.
theorem Th31: :: WAYBEL29:31
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):] )
proofend;

:: 4.11. THEOREM, (2) <=> (3+), p. 133.
theorem Th32: :: WAYBEL29:32
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):] )
proofend;

:: 4.11. THEOREM, (1) <=> (3+), p. 133.
theorem :: WAYBEL29:33
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):] )
proofend;