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

begin

definition

let F be Function;
attr F 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 ) );
attr F 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 ) );
attr F 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 set ;
coherence
for b₁ being Function st b₁ is empty holds
( b₁ is uncurrying & b₁ is currying & b₁ is commuting )

proof end;

end;

registration

cluster Relation-like Function-like uncurrying currying commuting set ;
existence
ex b₁ being Function st
( b₁ is uncurrying & b₁ is currying & b₁ is commuting )

proof end;

end;

registration

let F be uncurrying Function;
let X be set ;
cluster F | X -> uncurrying ;
coherence
F | X is uncurrying

proof end;

end;

registration

let F be currying Function;
let X be set ;
cluster F | X -> currying ;
coherence
F | X is currying

proof end;

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

proof end;

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

proof end;

registration

let X, Y, Z be set ;
cluster Relation-like Funcs (X,(Funcs (Y,Z))) -defined Function-like V24( Funcs (X,(Funcs (Y,Z)))) uncurrying set ;
existence
ex b₁ being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st b₁ is uncurrying

proof end;

cluster Relation-like Funcs ([:X,Y:],Z) -defined Function-like V24( Funcs ([:X,Y:],Z)) currying set ;
existence
ex b₁ being ManySortedSet of Funcs ([:X,Y:],Z) st b₁ is currying

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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}:]

proof end;

registration

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

proof end;

end;

registration

cluster non empty constituted-Functions strict reflexive transitive antisymmetric V209() V210() complete non void RelStr ;
existence
ex b₁ being LATTICE st
( b₁ is constituted-Functions & b₁ is complete & b₁ is strict )

proof end;

cluster non empty constituted-Functions 1-sorted ;
existence
ex b₁ being 1-sorted st
( b₁ is constituted-Functions & not b₁ is empty )

proof end;

end;

registration

let T be non empty constituted-Functions RelStr ;
cluster non empty -> non empty constituted-Functions SubRelStr of T;
coherence
for b₁ being non empty SubRelStr of T holds b₁ is constituted-Functions

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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 func f . x -> Element of T;
coherence
f . x is Element of T

proof end;

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 )

proof end;

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

proof end;

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

proof end;

theorem Th17: :: WAYBEL27:17

for X being set ex f being Function of (BoolePoset X),((BoolePoset 1) |^ X) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )

proof end;

theorem Th18: :: WAYBEL27:18

for X being set holds BoolePoset X,(BoolePoset 1) |^ X are_isomorphic

proof end;

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

proof end;

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

proof end;

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

proof end;

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 & ( for x being set holds
( x in the carrier of it iff x is directed-sups-preserving Function of S,T ) ) );
existence
ex b₁ being strict RelStr st
( b₁ is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b₁ iff x is directed-sups-preserving Function of S,T ) ) )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st b₁ is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b₁ iff x is directed-sups-preserving Function of S,T ) ) & b₂ is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b₂ iff x is directed-sups-preserving Function of S,T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines UPS WAYBEL27:def 4 :
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for b₃ being strict RelStr holds
( b₃ = UPS (S,T) iff ( b₃ is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b₃ 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 & UPS (S,T) is reflexive & UPS (S,T) is antisymmetric & UPS (S,T) is constituted-Functions )

proof end;

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

proof end;

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)

proof end;

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 func f . s -> Element of T;
coherence
f . s is Element of T

proof end;

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 )

proof end;

theorem Th24: :: WAYBEL27:24

for S, T being complete Scott TopLattice holds UPS (S,T) = SCMaps (S,T)

proof end;

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

proof end;

registration

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

proof end;

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

proof end;

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

proof end;

definition

let S1, S2, T1, T2 be non empty reflexive antisymmetric RelStr ;
let f be Function of S1,S2;
assume A1: 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 b₁ being Function of (UPS (S2,T1)),(UPS (S1,T2)) st
for h being directed-sups-preserving Function of S2,T1 holds b₁ . h = (g * h) * f

proof end;

uniqueness
for b₁, b₂ being Function of (UPS (S2,T1)),(UPS (S1,T2)) st ( for h being directed-sups-preserving Function of S2,T1 holds b₁ . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds b₂ . h = (g * h) * f ) holds
b₁ = b₂

proof end;

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 b₇ being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds
( b₇ = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b₇ . h = (g * h) * f );

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

proof end;

theorem Th29: :: WAYBEL27:29

for S, T being non empty reflexive antisymmetric RelStr holds UPS ((id S),(id T)) = id (UPS (S,T))

proof end;

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

proof end;

theorem Th31: :: WAYBEL27:31

Omega Sierpinski_Space is Scott

proof end;

theorem :: WAYBEL27:32

for S being complete Scott TopLattice holds oContMaps (S,Sierpinski_Space) = UPS (S,(BoolePoset 1))

proof end;

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 & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) )

proof end;

theorem Th34: :: WAYBEL27:34

for S being complete LATTICE holds UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic

proof end;

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 & g is isomorphic holds
UPS (f,g) is isomorphic

proof end;

theorem Th36: :: WAYBEL27:36

for S1, S2, T1, T2 being complete LATTICE st S1,S2 are_isomorphic & T1,T2 are_isomorphic holds
UPS (S2,T1), UPS (S1,T2) are_isomorphic

proof end;

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

proof end;

Lm1: now

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))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & 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))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & 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))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & 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) & dom (commute f) = M )
then commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:85;
then ex g being Function st
( commute f = g & dom g = M & 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) & 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

proof end;

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

proof end;

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)

proof end;

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 & F is isomorphic )

proof end;

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

proof end;

theorem :: WAYBEL27:43

for S, T being complete continuous LATTICE holds UPS (S,T) is continuous

proof end;

theorem :: WAYBEL27:44

for S, T being complete algebraic LATTICE holds UPS (S,T) is algebraic

proof end;

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

proof end;

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

proof end;

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 & f is isomorphic )

proof end;