:: Continuous Lattices between T$_0$ Spaces
:: by Grzegorz Bancerek
::
:: Received September 24, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

notation
let I be set ;
let J be RelStr-yielding ManySortedSet of I;
synonym I -POS_prod J for  product J;
end;

notation
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
synonym I -TOP_prod J for  product J;
end;

:: 4.1. DEFINITION (a)
definition
let X, Y be non empty TopSpace;
func oContMaps (X,Y) ->  non empty strict RelStr  equals :: WAYBEL26:def 1
 ContMaps (X,(Omega Y));
coherence
 ContMaps (X,(Omega Y)) is non empty strict RelStr ;
end;

:: deftheorem  defines oContMaps WAYBEL26:def_1_:_
 for X, Y being non empty TopSpace holds oContMaps (X,Y) = ContMaps (X,(Omega Y));

registration
let X, Y be non empty TopSpace;
cluster oContMaps (X,Y) ->  non empty constituted-Functions strict reflexive transitive ;
coherence
 ( oContMaps (X,Y) is reflexive & oContMaps (X,Y) is transitive & oContMaps (X,Y) is constituted-Functions ) ;
end;

registration
let X be non empty TopSpace;
let Y be non empty T_0 TopSpace;
cluster oContMaps (X,Y) ->  non empty strict antisymmetric ;
coherence
 oContMaps (X,Y) is antisymmetric ;
end;

theorem Th1: :: WAYBEL26:1
for X, Y being non empty TopSpace
for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )
proofend;

theorem Th2: :: WAYBEL26:2
for X, Y being non empty TopSpace
for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,Y )
proofend;

theorem Th3: :: WAYBEL26:3
for X, Y being non empty TopSpace
for a, b being Element of (oContMaps (X,Y))
for f, g being Function of X,(Omega Y) st a = f & b = g holds
( a <= b iff f <= g )
proofend;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let A be Subset of (oContMaps (X,Y));
:: original:pi
redefine func pi (A,x) ->  Subset of (Omega Y);
coherence
 pi (A,x) is Subset of (Omega Y)
proofend;
end;

registration
let X, Y be non empty TopSpace;
let x be set ;
let A be non empty Subset of (oContMaps (X,Y));
cluster pi (A,x) ->  non empty ;
coherence
 not pi (A,x) is empty
proofend;
end;

theorem Th4: :: WAYBEL26:4
Omega Sierpinski_Space is TopAugmentation of BoolePoset 1
proofend;

theorem Th5: :: WAYBEL26:5
for X being non empty TopSpace ex f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) st
( f is isomorphic &amp; ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )
proofend;

theorem Th6: :: WAYBEL26:6
for X being non empty TopSpace holds InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic
proofend;

:: 4.1. DEFINITION (b)
definition
let X, Y, Z be non empty TopSpace;
let f be continuous Function of Y,Z;
func oContMaps (X,f) ->  Function of (oContMaps (X,Y)),(oContMaps (X,Z)) means :Def2: :: WAYBEL26:def 2
 for g being continuous Function of X,Y holds it . g = f * g;
uniqueness
 for b1, b2 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st ( for g being continuous Function of X,Y holds b1 . g = f * g ) &amp; ( for g being continuous Function of X,Y holds b2 . g = f * g ) holds
b1 = b2
proofend;
existence
 ex b1 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st
for g being continuous Function of X,Y holds b1 . g = f * g
proofend;
func oContMaps (f,X) ->  Function of (oContMaps (Z,X)),(oContMaps (Y,X)) means :Def3: :: WAYBEL26:def 3
 for g being continuous Function of Z,X holds it . g = g * f;
uniqueness
 for b1, b2 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st ( for g being continuous Function of Z,X holds b1 . g = g * f ) &amp; ( for g being continuous Function of Z,X holds b2 . g = g * f ) holds
b1 = b2
proofend;
existence
 ex b1 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st
for g being continuous Function of Z,X holds b1 . g = g * f
proofend;
end;

:: deftheorem Def2 defines oContMaps WAYBEL26:def_2_:_
 for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for b5 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) holds
( b5 = oContMaps (X,f) iff for g being continuous Function of X,Y holds b5 . g = f * g );

:: deftheorem Def3 defines oContMaps WAYBEL26:def_3_:_
 for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for b5 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) holds
( b5 = oContMaps (f,X) iff for g being continuous Function of Z,X holds b5 . g = g * f );

theorem Th7: :: WAYBEL26:7
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace holds oContMaps (X,Y) is up-complete
proofend;

theorem Th8: :: WAYBEL26:8
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z holds oContMaps (X,f) is monotone
proofend;

theorem :: WAYBEL26:9
for X, Y being non empty TopSpace
for f being continuous Function of Y,Y st f is idempotent holds
oContMaps (X,f) is idempotent
proofend;

theorem Th10: :: WAYBEL26:10
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z holds oContMaps (f,X) is monotone
proofend;

theorem Th11: :: WAYBEL26:11
for X, Y being non empty TopSpace
for f being continuous Function of Y,Y st f is idempotent holds
oContMaps (f,X) is idempotent
proofend;

theorem Th12: :: WAYBEL26:12
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for x being Element of X
for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
proofend;

:: 4.2. LEMMA (ii)
theorem Th13: :: WAYBEL26:13
for X being non empty TopSpace
for Y, Z being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving
proofend;

theorem Th14: :: WAYBEL26:14
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for x being Element of Y
for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))
proofend;

theorem Th15: :: WAYBEL26:15
for Y, Z being non empty TopSpace
for X being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving
proofend;

:: 4.3. LEMMA (i) genralized
theorem Th16: :: WAYBEL26:16
for X, Z being non empty TopSpace
for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
proofend;

theorem Th17: :: WAYBEL26:17
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
proofend;

Lm1:  for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
proofend;

theorem Th18: :: WAYBEL26:18
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
proofend;

theorem Th19: :: WAYBEL26:19
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)
proofend;

theorem Th20: :: WAYBEL26:20
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z st f is being_homeomorphism holds
oContMaps (X,f) is isomorphic
proofend;

theorem Th21: :: WAYBEL26:21
for X, Y, Z being non empty TopSpace st Y,Z are_homeomorphic holds
oContMaps (X,Y), oContMaps (X,Z) are_isomorphic
proofend;

:: 4.3. LEMMA (ii)
theorem Th22: :: WAYBEL26:22
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z &amp; oContMaps (X,Z) is complete &amp; oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete &amp; oContMaps (X,Y) is continuous )
proofend;

theorem Th23: :: WAYBEL26:23
for X being non empty TopSpace
for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z &amp; oContMaps (X,Z) is complete &amp; oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete &amp; oContMaps (X,Y) is continuous )
proofend;

theorem Th24: :: WAYBEL26:24
for Y being non trivial T_0-TopSpace st not Y is T_1 holds
Sierpinski_Space is_Retract_of Y
proofend;

theorem Th25: :: WAYBEL26:25
for X being non empty TopSpace
for Y being non trivial T_0-TopSpace st oContMaps (X,Y) is with_suprema holds
not Y is T_1
proofend;

registration
cluster Sierpinski_Space  ->  non trivial monotone-convergence ;
coherence
 ( not Sierpinski_Space is trivial &amp; Sierpinski_Space is monotone-convergence )
proofend;
end;

registration
cluster non empty non trivial TopSpace-like T_0 injective monotone-convergence for TopStruct ;
existence
 ex b1 being T_0-TopSpace st
( b1 is injective &amp; b1 is monotone-convergence &amp; not b1 is trivial )
proofend;
end;

:: 4.4. PROPOSITION
theorem Th26: :: WAYBEL26:26
for X being non empty TopSpace
for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete &amp; oContMaps (X,Y) is continuous holds
InclPoset the topology of X is continuous
proofend;

theorem Th27: :: WAYBEL26:27
for X being non empty TopSpace
for x being Point of X
for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) &amp; ex h being continuous Function of X,X st
( h = X --> x &amp; F = oContMaps (h,Y) ) )
proofend;

:: 4.5. PROPOSITION
theorem Th28: :: WAYBEL26:28
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete &amp; oContMaps (X,Y) is continuous holds
( Omega Y is complete &amp; Omega Y is continuous )
proofend;

theorem Th29: :: WAYBEL26:29
for X being non empty 1-sorted
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj (J,i)) * f
proofend;

theorem Th30: :: WAYBEL26:30
for S being 1-sorted
for M being set holds Carrier (M --> S) = M --> the carrier of S
proofend;

theorem Th31: :: WAYBEL26:31
for X, Y being non empty TopSpace
for M being non empty set
for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M, the carrier of (oContMaps (X,Y))
proofend;

theorem Th32: :: WAYBEL26:32
for X, Y being non empty TopSpace holds the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y)
proofend;

theorem Th33: :: WAYBEL26:33
for X, Y being non empty TopSpace
for M being non empty set
for f being Function of M, the carrier of (oContMaps (X,Y)) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
proofend;

theorem Th34: :: WAYBEL26:34
for X being non empty TopSpace
for M being non empty set ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st
( F is isomorphic &amp; ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
proofend;

theorem Th35: :: WAYBEL26:35
for X being non empty TopSpace
for M being non empty set holds oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))),M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))) are_isomorphic
proofend;

:: 4.6. PROPOSITION
theorem Th36: :: WAYBEL26:36
for X being non empty TopSpace st InclPoset the topology of X is continuous holds
for Y being injective T_0-TopSpace holds
( oContMaps (X,Y) is complete &amp; oContMaps (X,Y) is continuous )
proofend;

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

:: 4.7. THEOREM p.129.
theorem :: WAYBEL26:37
for X being non empty TopSpace
for L being non trivial complete Scott TopLattice holds
( oContMaps (X,L) is complete &amp; oContMaps (X,L) is continuous iff ( InclPoset the topology of X is continuous &amp; L is continuous ) )
proofend;

registration
let f be Function;
cluster Union (disjoin f) ->  Relation-like ;
coherence
 Union (disjoin f) is Relation-like
proofend;
end;

definition
let f be Function;
func *graph f ->  Relation equals :: WAYBEL26:def 4
(Union (disjoin f)) ~ ;
correctness
coherence
(Union (disjoin f)) ~ is Relation;
;
end;

:: deftheorem  defines *graph WAYBEL26:def_4_:_
 for f being Function holds *graph f = (Union (disjoin f)) ~ ;

theorem Th38: :: WAYBEL26:38
for x, y being set
for f being Function holds
( [x,y] in *graph f iff ( x in dom f &amp; y in f . x ) )
proofend;

theorem Th39: :: WAYBEL26:39
for X being finite set holds
( proj1 X is finite &amp; proj2 X is finite )
proofend;

:: 4.8. LEMMA p.130.
theorem Th40: :: WAYBEL26:40
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
proofend;

definition
let W be Relation;
let X be set ;
func(W,X) *graph  ->  Function means :Def5: :: WAYBEL26:def 5
( dom it = X &amp; ( for x being set st x in X holds
it . x = Im (W,x) ) );
existence
 ex b1 being Function st
( dom b1 = X &amp; ( for x being set st x in X holds
b1 . x = Im (W,x) ) )
proofend;
correctness
uniqueness
for b1, b2 being Function st dom b1 = X &amp; ( for x being set st x in X holds
b1 . x = Im (W,x) ) &amp; dom b2 = X &amp; ( for x being set st x in X holds
b2 . x = Im (W,x) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def5 defines *graph WAYBEL26:def_5_:_
 for W being Relation
for X being set
for b3 being Function holds
( b3 = (W,X) *graph iff ( dom b3 = X &amp; ( for x being set st x in X holds
b3 . x = Im (W,x) ) ) );

theorem Th41: :: WAYBEL26:41
for W being Relation
for X being set st dom W c= X holds
*graph ((W,X) *graph) = W
proofend;

registration
let X, Y be TopSpace;
cluster  ->  Relation-like for Element of bool the carrier of [:X,Y:];
coherence
 for b1 being Subset of [:X,Y:] holds b1 is Relation-like
proofend;
cluster  ->  Relation-like for Element of the topology of [:X,Y:];
coherence
 for b1 being Element of the topology of [:X,Y:] holds b1 is Relation-like ;
end;

theorem Th42: :: WAYBEL26:42
for X, Y being non empty TopSpace
for W being open Subset of [:X,Y:]
for x being Point of X holds Im (W,x) is open Subset of Y
proofend;

:: 4.9. PROPOSITION a) p.130.
theorem Th43: :: WAYBEL26:43
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W being open Subset of [:X,Y:] holds (W, the carrier of X) *graph is continuous Function of X,S
proofend;

:: 4.9. PROPOSITION b) p.130.
theorem Th44: :: WAYBEL26:44
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds
for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph &amp; f2 = (W2, the carrier of X) *graph holds
f1 <= f2
proofend;

:: 4.9. PROPOSITION p.130.
theorem :: WAYBEL26:45
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) st
( F is monotone &amp; ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
proofend;