WAYBEL27: Function Spaces in the Category of Directed Suprema Preserving Maps

:: Function Spaces in the Category of Directed Suprema Preserving Maps
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received November 26, 1999
:: Copyright (c) 1999 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 :

:: deftheorem Def2 defines currying WAYBEL27:def 2 :

:: deftheorem Def3 defines commuting WAYBEL27:def 3 :

registration

cluster empty -> uncurrying currying commuting set ;
coherence

proof end;

end;

registration

cluster uncurrying currying commuting set ;
existence

proof end;

end;

registration

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

proof end;

end;

registration

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

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 uncurrying set ;
existence

proof end;

cluster currying set ;
existence

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 X be set ;
let Y be non empty functional set ;
cluster -> Function-yielding Element of bool [:X,Y:];
coherence

proof end;

end;

registration

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

proof end;

end;

registration

cluster constituted-Functions strict complete RelStr ;
existence

proof end;

cluster non empty constituted-Functions 1-sorted ;
existence

proof end;

end;

registration

let T be non empty constituted-Functions RelStr ;
cluster non empty -> non empty constituted-Functions SubRelStr of T;
coherence

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines UPS WAYBEL27:def 4 :

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

proof end;

end;

registration

let S be non empty RelStr ;
let T be non empty Poset;
cluster UPS S,T -> strict transitive ;
coherence

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

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, S' being non empty RelStr
for T, T' being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) holds
UPS S,T = UPS S',T'

proof end;

registration

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines UPS WAYBEL27:def 5 :

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:
let X, Y be non empty Poset; :: thesis:
let f be directed-sups-preserving Function of X,(Y |^ M); :: thesis:
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:
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:

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;