:: Function Spaces in the Category of Directed Suprema Preserving Maps
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received November 26, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

definition
let F be Function;
attrF is uncurrying  means :Def1: :: WAYBEL27:def 1
( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = uncurry f ) );
attrF is currying  means :Def2: :: WAYBEL27:def 2
( ( for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds
F . f = curry f ) );
attrF is commuting  means :Def3: :: WAYBEL27:def 3
( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = commute f ) );
end;

:: deftheorem Def1 defines uncurrying WAYBEL27:def_1_:_
 for F being Function holds
( F is uncurrying iff ( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = uncurry f ) ) );

:: deftheorem Def2 defines currying WAYBEL27:def_2_:_
 for F being Function holds
( F is currying iff ( ( for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds
F . f = curry f ) ) );

:: deftheorem Def3 defines commuting WAYBEL27:def_3_:_
 for F being Function holds
( F is commuting iff ( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = commute f ) ) );

registration
cluster empty Relation-like Function-like  ->  uncurrying currying commuting for set ;
coherence
 for b1 being Function st b1 is empty holds
( b1 is uncurrying & b1 is currying & b1 is commuting )
proofend;
end;

registration
cluster Relation-like Function-like uncurrying currying commuting for set ;
existence
 ex b1 being Function st
( b1 is uncurrying & b1 is currying & b1 is commuting )
proofend;
end;

registration
let F be uncurrying Function;
let X be set ;
clusterF | X ->  uncurrying ;
coherence
 F | X is uncurrying
proofend;
end;

registration
let F be currying Function;
let X be set ;
clusterF | X ->  currying ;
coherence
 F | X is currying
proofend;
end;

theorem Th1: :: WAYBEL27:1
for X, Y, Z, D being set st D c= Funcs (X,(Funcs (Y,Z))) holds
ex F being ManySortedSet of D st
( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )
proofend;

theorem Th2: :: WAYBEL27:2
for X, Y, Z, D being set st D c= Funcs ([:X,Y:],Z) holds
ex F being ManySortedSet of D st
( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )
proofend;

registration
let X, Y, Z be set ;
cluster Relation-like Funcs (X,(Funcs (Y,Z))) -defined Function-like V27( Funcs (X,(Funcs (Y,Z)))) uncurrying for set ;
existence
 ex b1 being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st b1 is uncurrying
proofend;
cluster Relation-like Funcs ([:X,Y:],Z) -defined Function-like V27( Funcs ([:X,Y:],Z)) currying for set ;
existence
 ex b1 being ManySortedSet of Funcs ([:X,Y:],Z) st b1 is currying
proofend;
end;

theorem Th3: :: WAYBEL27:3
for A, B being non empty set
for C being set
for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)
proofend;

theorem Th4: :: WAYBEL27:4
for B being non empty set
for A, C being set
for f being uncurrying Function
for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)
proofend;

theorem Th5: :: WAYBEL27:5
for A, B, C being set
for f being currying Function
for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds
g * f = id (dom f)
proofend;

theorem Th6: :: WAYBEL27:6
for f being Function-yielding Function
for i, A being set st i in dom (commute f) holds
((commute f) . i) .: A c= pi ((f .: A),i)
proofend;

theorem Th7: :: WAYBEL27:7
for f being Function-yielding Function
for i, A being set st ( for g being Function st g in f .: A holds
i in dom g ) holds
pi ((f .: A),i) c= ((commute f) . i) .: A
proofend;

theorem Th8: :: WAYBEL27:8
for X, Y being set
for f being Function st rng f c= Funcs (X,Y) holds
for i, A being set st i in X holds
((commute f) . i) .: A = pi ((f .: A),i)
proofend;

theorem Th9: :: WAYBEL27:9
for f being Function
for i, A being set st [:A,{i}:] c= dom f holds
pi (((curry f) .: A),i) = f .: [:A,{i}:]
proofend;

registration
let T be constituted-Functions 1-sorted ;
cluster the carrier of T ->  functional ;
coherence
 the carrier of T is functional
proofend;
end;

registration
cluster non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete non void for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is constituted-Functions & b1 is complete & b1 is strict )
proofend;
cluster non empty constituted-Functions for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is constituted-Functions & not b1 is empty )
proofend;
end;

registration
let T be non empty constituted-Functions RelStr ;
cluster non empty  ->  non empty constituted-Functions for SubRelStr of T;
coherence
 for b1 being non empty SubRelStr of T holds b1 is constituted-Functions
proofend;
end;

theorem Th10: :: WAYBEL27:10
for S, T being complete LATTICE
for f being idempotent Function of T,T
for h being Function of S,(Image f) holds f * h = h
proofend;

theorem :: WAYBEL27:11
for S, T, T1 being non empty RelStr st T is SubRelStr of T1 holds
for f being Function of S,T
for f1 being Function of S,T1 st f is monotone & f = f1 holds
f1 is monotone
proofend;

theorem Th12: :: WAYBEL27:12
for S, T, T1 being non empty RelStr st T is full SubRelStr of T1 holds
for f being Function of S,T
for f1 being Function of S,T1 st f1 is monotone & f = f1 holds
f is monotone
proofend;

theorem Th13: :: WAYBEL27:13
for X being set
for V being Subset of X holds
( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V )
proofend;

begin

definition
let X be non empty set ;
let T be non empty RelStr ;
let f be Element of (T |^ X);
let x be Element of X;
:: original:.
redefine funcf . x ->  Element of T;
coherence
 f . x is Element of T
proofend;
end;

theorem Th14: :: WAYBEL27:14
for X being non empty set
for T being non empty RelStr
for f, g being Element of (T |^ X) holds
( f <= g iff for x being Element of X holds f . x <= g . x )
proofend;

theorem Th15: :: WAYBEL27:15
for X being set
for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds
L |^ X = S |^ X
proofend;

theorem :: WAYBEL27:16
for S1, S2, T1, T2 being non empty TopSpace st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) &amp; TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
oContMaps (S1,T1) = oContMaps (S2,T2)
proofend;

theorem Th17: :: WAYBEL27:17
for X being set ex f being Function of (BoolePoset X),((BoolePoset 1) |^ X) st
( f is isomorphic &amp; ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
proofend;

theorem Th18: :: WAYBEL27:18
for X being set holds BoolePoset X,(BoolePoset 1) |^ X are_isomorphic
proofend;

theorem Th19: :: WAYBEL27:19
for X, Y being non empty set
for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ X) |^ Y
for S2 being non empty full SubRelStr of (T |^ Y) |^ X
for F being Function of S1,S2 st F is commuting holds
F is monotone
proofend;

theorem Th20: :: WAYBEL27:20
for X, Y being non empty set
for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S1,S2 st F is uncurrying holds
F is monotone
proofend;

theorem Th21: :: WAYBEL27:21
for X, Y being non empty set
for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S2,S1 st F is currying holds
F is monotone
proofend;

begin

definition
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
func UPS (S,T) ->  strict RelStr  means :Def4: :: WAYBEL27:def 4
( it is full SubRelStr of T |^ the carrier of S &amp; ( for x being set holds
( x in the carrier of it iff x is directed-sups-preserving Function of S,T ) ) );
existence
 ex b1 being strict RelStr st
( b1 is full SubRelStr of T |^ the carrier of S &amp; ( for x being set holds
( x in the carrier of b1 iff x is directed-sups-preserving Function of S,T ) ) )
proofend;
uniqueness
 for b1, b2 being strict RelStr st b1 is full SubRelStr of T |^ the carrier of S &amp; ( for x being set holds
( x in the carrier of b1 iff x is directed-sups-preserving Function of S,T ) ) &amp; b2 is full SubRelStr of T |^ the carrier of S &amp; ( for x being set holds
( x in the carrier of b2 iff x is directed-sups-preserving Function of S,T ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines UPS WAYBEL27:def_4_:_
 for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for b3 being strict RelStr holds
( b3 = UPS (S,T) iff ( b3 is full SubRelStr of T |^ the carrier of S &amp; ( for x being set holds
( x in the carrier of b3 iff x is directed-sups-preserving Function of S,T ) ) ) );

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
cluster UPS (S,T) ->  non empty constituted-Functions strict reflexive antisymmetric ;
coherence
 ( not UPS (S,T) is empty &amp; UPS (S,T) is reflexive &amp; UPS (S,T) is antisymmetric &amp; UPS (S,T) is constituted-Functions )
proofend;
end;

registration
let S be non empty RelStr ;
let T be non empty Poset;
cluster UPS (S,T) ->  strict transitive ;
coherence
 UPS (S,T) is transitive
proofend;
end;

theorem Th22: :: WAYBEL27:22
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T)
proofend;

definition
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric RelStr ;
let f be Element of (UPS (S,T));
let s be Element of S;
:: original:.
redefine funcf . s ->  Element of T;
coherence
 f . s is Element of T
proofend;
end;

theorem Th23: :: WAYBEL27:23
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for f, g being Element of (UPS (S,T)) holds
( f <= g iff for s being Element of S holds f . s <= g . s )
proofend;

theorem Th24: :: WAYBEL27:24
for S, T being complete Scott TopLattice holds UPS (S,T) = SCMaps (S,T)
proofend;

theorem Th25: :: WAYBEL27:25
for S, S9 being non empty RelStr
for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) &amp; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds
UPS (S,T) = UPS (S9,T9)
proofend;

registration
let S, T be complete LATTICE;
cluster UPS (S,T) ->  strict complete ;
coherence
 UPS (S,T) is complete
proofend;
end;

theorem Th26: :: WAYBEL27:26
for S, T being complete LATTICE holds UPS (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
proofend;

theorem Th27: :: WAYBEL27:27
for S, T being complete LATTICE
for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S))
proofend;

definition
let S1, S2, T1, T2 be non empty reflexive antisymmetric RelStr ;
let f be Function of S1,S2;
assume B1: f is directed-sups-preserving ;
let g be Function of T1,T2;
assume A2: g is directed-sups-preserving ;
func UPS (f,g) ->  Function of (UPS (S2,T1)),(UPS (S1,T2)) means :Def5: :: WAYBEL27:def 5
 for h being directed-sups-preserving Function of S2,T1 holds it . h = (g * h) * f;
existence
 ex b1 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st
for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f
proofend;
uniqueness
 for b1, b2 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st ( for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f ) &amp; ( for h being directed-sups-preserving Function of S2,T1 holds b2 . h = (g * h) * f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines UPS WAYBEL27:def_5_:_
 for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of S1,S2 st f is directed-sups-preserving holds
for g being Function of T1,T2 st g is directed-sups-preserving holds
for b7 being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds
( b7 = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b7 . h = (g * h) * f );

:: 2.6. PROPOSITOION, p. 115
:: preservation of composition
theorem Th28: :: WAYBEL27:28
for S1, S2, S3, T1, T2, T3 being non empty Poset
for f1 being directed-sups-preserving Function of S2,S3
for f2 being directed-sups-preserving Function of S1,S2
for g1 being directed-sups-preserving Function of T1,T2
for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1))
proofend;

:: 2.6. PROPOSITOION, p. 115
:: preservation of identities
theorem Th29: :: WAYBEL27:29
for S, T being non empty reflexive antisymmetric RelStr holds UPS ((id S),(id T)) = id (UPS (S,T))
proofend;

:: 2.6. PROPOSITOION, p. 115
:: preservation of directed-sups
theorem Th30: :: WAYBEL27:30
for S1, S2, T1, T2 being complete LATTICE
for f being directed-sups-preserving Function of S1,S2
for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving
proofend;

theorem Th31: :: WAYBEL27:31
Omega Sierpinski_Space is Scott
proofend;

theorem :: WAYBEL27:32
for S being complete Scott TopLattice holds oContMaps (S,Sierpinski_Space) = UPS (S,(BoolePoset 1))
proofend;

:: 2.7. LEMMA, p. 116
theorem Th33: :: WAYBEL27:33
for S being complete LATTICE ex F being Function of (UPS (S,(BoolePoset 1))),(InclPoset (sigma S)) st
( F is isomorphic &amp; ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) )
proofend;

theorem Th34: :: WAYBEL27:34
for S being complete LATTICE holds UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic
proofend;

theorem Th35: :: WAYBEL27:35
for S1, S2, T1, T2 being complete LATTICE
for f being Function of S1,S2
for g being Function of T1,T2 st f is isomorphic &amp; g is isomorphic holds
UPS (f,g) is isomorphic
proofend;

theorem Th36: :: WAYBEL27:36
for S1, S2, T1, T2 being complete LATTICE st S1,S2 are_isomorphic &amp; T1,T2 are_isomorphic holds
UPS (S2,T1), UPS (S1,T2) are_isomorphic
proofend;

theorem Th37: :: WAYBEL27:37
for S, T being complete LATTICE
for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f))
proofend;

Lm1: now__::_thesis:_for_M_being_non_empty_set_
for_X,_Y_being_non_empty_Poset
for_f_being_directed-sups-preserving_Function_of_X,(Y_|^_M)_holds_
(_f_in_Funcs_(_the_carrier_of_X,(Funcs_(M,_the_carrier_of_Y)))_&amp;_rng_(commute_f)_c=_Funcs_(_the_carrier_of_X,_the_carrier_of_Y)_&amp;_dom_(commute_f)_=_M_)
let M be non empty set ; ::_thesis: for X, Y being non empty Poset
for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) &amp; rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) &amp; dom (commute f) = M )
let X, Y be non empty Poset; ::_thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) &amp; rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) &amp; dom (commute f) = M )
let f be directed-sups-preserving Function of X,(Y |^ M); ::_thesis: ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) &amp; rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) &amp; dom (commute f) = M )
 the carrier of (Y |^ M) = Funcs (M, the carrier of Y) by YELLOW_1:28;
then A1: rng f c= Funcs (M, the carrier of Y) ;
 dom f = the carrier of X by FUNCT_2:def_1;
hence  f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by A1, FUNCT_2:def_2; ::_thesis: ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) &amp; dom (commute f) = M )
then  commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:55;
then  ex g being Function st
( commute f = g &amp; dom g = M &amp; rng g c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def_2;
hence  ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) &amp; dom (commute f) = M ) ; ::_thesis: verum
end;

theorem Th38: :: WAYBEL27:38
for X being non empty set
for S, T being non empty Poset
for f being directed-sups-preserving Function of S,(T |^ X)
for i being Element of X holds (commute f) . i is directed-sups-preserving Function of S,T
proofend;

theorem Th39: :: WAYBEL27:39
for X being non empty set
for S, T being non empty Poset
for f being directed-sups-preserving Function of S,(T |^ X) holds commute f is Function of X, the carrier of (UPS (S,T))
proofend;

theorem Th40: :: WAYBEL27:40
for X being non empty set
for S, T being non empty Poset
for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)
proofend;

theorem Th41: :: WAYBEL27:41
for X being non empty set
for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st
( F is commuting &amp; F is isomorphic )
proofend;

theorem Th42: :: WAYBEL27:42
for X being non empty set
for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic
proofend;

:: 2.8. THEOREM, p. 116
:: [CONT -> CONT] is into CONT (so [CONT -> CONT] is functor)
theorem :: WAYBEL27:43
for S, T being complete continuous LATTICE holds UPS (S,T) is continuous
proofend;

:: 2.8. THEOREM, p. 116
:: [ALG -> ALG] is into ALG (so [ALG -> ALG] is functor)
theorem :: WAYBEL27:44
for S, T being complete algebraic LATTICE holds UPS (S,T) is algebraic
proofend;

theorem Th45: :: WAYBEL27:45
for R, S, T being complete LATTICE
for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T
proofend;

theorem Th46: :: WAYBEL27:46
for R, S, T being complete LATTICE
for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T))
proofend;

:: 2.10. THEOREM, p. 117
theorem :: WAYBEL27:47
for R, S, T being complete LATTICE ex f being Function of (UPS (R,(UPS (S,T)))),(UPS ([:R,S:],T)) st
( f is uncurrying &amp; f is isomorphic )
proofend;