:: Function Spaces in the Category of Directed Suprema Preserving Maps
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received November 26, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, RELAT_1, FUNCOP_1, FUNCT_5, FUNCT_6, XBOOLE_0, TARSKI,
FUNCT_2, PBOOLE, ZFMISC_1, SUBSET_1, CARD_3, MCART_1, MONOID_0, STRUCT_0,
REWRITE1, WAYBEL_0, NEWTON, ORDERS_2, YELLOW_0, BINOP_1, GROUP_6, SEQM_3,
XXREAL_0, CAT_1, FUNCT_3, CARD_1, YELLOW_1, RLVECT_2, PRE_TOPC, WAYBEL26,
WAYBEL24, WAYBEL25, ORDINAL2, RCOMP_1, WELLORD2, WELLORD1, RELAT_2,
WAYBEL11, WAYBEL_9, WAYBEL17, YELLOW_9, EQREL_1, WAYBEL18, PROB_1,
WAYBEL_1, WAYBEL_8, RLVECT_3, LATTICES, BORSUK_1, WAYBEL27;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, TOLER_1, MCART_1,
RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4,
FUNCT_5, ORDINAL1, NUMBERS, CARD_3, FUNCOP_1, FUNCT_6, ORDERS_1,
MONOID_0, PRALG_1, QUANTAL1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC,
TOPS_2, ORDERS_2, CANTOR_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1,
YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11,
YELLOW_9, WAYBEL17, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26;
constructors DOMAIN_1, TOLER_1, FUNCT_6, TOPS_2, CANTOR_1, MONOID_0, QUANTAL1,
ORDERS_3, WAYBEL_6, WAYBEL_8, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24,
YELLOW16, WAYBEL26, RELSET_1, WAYBEL20, FUNCT_5, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
STRUCT_0, TOPS_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1,
YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL10,
WAYBEL14, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL24, WAYBEL25,
YELLOW16, RELSET_1, XTUPLE_0, FUNCT_5;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, MONOID_0, WAYBEL_0, FUNCOP_1, WAYBEL_1, XBOOLE_0;
equalities BINOP_1, YELLOW_2, STRUCT_0, ORDINAL1;
expansions TARSKI, FUNCT_1, WAYBEL_0, WAYBEL_1;
theorems YELLOW_1, CARD_3, FUNCT_2, FUNCT_1, PRE_TOPC, TARSKI, PRALG_1,
FUNCOP_1, YELLOW_0, WELLORD1, WAYBEL17, WAYBEL10, TOPS_2, TOPS_3,
YELLOW_9, WAYBEL24, WAYBEL26, WAYBEL_0, RELSET_1, ORDERS_2, RELAT_1,
FUNCT_6, YELLOW14, WAYBEL18, WAYBEL20, WAYBEL25, WAYBEL_1, WAYBEL15,
QUANTAL1, WAYBEL14, WAYBEL13, YELLOW16, ZFMISC_1, FUNCT_5, FUNCT_3,
YELLOW_2, WAYBEL_3, WAYBEL_8, YELLOW_3, FUNCT_4, WAYBEL21, XBOOLE_0,
XBOOLE_1, PARTFUN1, XTUPLE_0, CARD_1;
schemes FUNCT_2, PBOOLE, XBOOLE_0;
begin
definition
let F be Function;
attr F is uncurrying means
:Def1:
(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:
(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:
(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;
registration
cluster empty -> uncurrying currying commuting for Function;
coherence;
end;
registration
cluster uncurrying currying commuting for Function;
existence
proof
reconsider F={} as Function;
take F;
thus thesis;
end;
end;
registration
let F be uncurrying Function, X be set;
cluster F|X -> uncurrying;
coherence
proof
A1: for f being Function st f in dom (F|X) holds (F|X).f = uncurry f
proof
let f be Function;
assume
A2: f in dom (F|X);
then
A3: f in dom F by RELAT_1:57;
thus (F|X).f = F.f by A2,FUNCT_1:47
.= uncurry f by A3,Def1;
end;
for x being set st x in dom (F|X) holds x is Function-yielding Function
proof
let x be set;
assume x in dom (F|X);
then x in dom F by RELAT_1:57;
hence thesis by Def1;
end;
hence thesis by A1;
end;
end;
registration
let F be currying Function, X be set;
cluster F|X -> currying;
coherence
proof
A1: for f being Function st f in dom (F|X) holds (F|X).f = curry f
proof
let f be Function;
assume
A2: f in dom (F|X);
then
A3: f in dom F by RELAT_1:57;
thus (F|X).f = F.f by A2,FUNCT_1:47
.= curry f by A3,Def2;
end;
for x being set st x in dom (F|X) holds x is Function & proj1 x is Relation
proof
let x be set;
assume x in dom (F|X);
then x in dom F by RELAT_1:57;
hence thesis by Def2;
end;
hence thesis by A1;
end;
end;
theorem Th1:
for X,Y,Z,D being set st D c= Funcs(X, Funcs(Y,Z)) ex F being
ManySortedSet of D st F is uncurrying & rng F c= Funcs([:X,Y:], Z)
proof
let X,Y,Z,D be set such that
A1: D c= Funcs(X, Funcs(Y,Z));
per cases;
suppose
D is empty;
then reconsider F={} as ManySortedSet of D by PARTFUN1:def 2,RELAT_1:38
,def 18;
take F;
thus F is uncurrying;
thus thesis;
end;
suppose
D is non empty;
then reconsider E=D as non empty functional set by A1;
deffunc F(Function) = uncurry $1;
consider F being ManySortedSet of E such that
A2: for d being Element of E holds F.d = F(d) from PBOOLE:sch 5;
reconsider F1=F as ManySortedSet of D;
take F1;
thus F1 is uncurrying
proof
hereby
let x be set;
assume x in dom F1;
then x in D;
then consider x1 being Function such that
A3: x1=x and
dom x1=X and
A4: rng x1 c= Funcs(Y,Z) by A1,FUNCT_2:def 2;
x1 is Function-yielding
proof
let a be object;
assume a in dom x1;
then x1.a in rng x1 by FUNCT_1:def 3;
hence thesis by A4;
end;
hence x is Function-yielding Function by A3;
end;
let f be Function;
assume f in dom F1;
then reconsider d=f as Element of E;
thus F1.f = F.d .= uncurry f by A2;
end;
thus rng F1 c= Funcs([:X,Y:], Z)
proof
let y be object;
assume y in rng F1;
then consider x being object such that
A5: x in dom F1 and
A6: y = F1.x by FUNCT_1:def 3;
reconsider d=x as Element of E by A5;
A7: d in Funcs(X, Funcs(Y,Z)) by A1;
y = uncurry d by A2,A6;
hence thesis by A7,FUNCT_6:11;
end;
end;
end;
theorem Th2:
for X,Y,Z,D being set st D c= Funcs([:X,Y:], Z) ex F being
ManySortedSet of D st F is currying & ((Y = {} implies X = {}) implies rng F c=
Funcs(X, Funcs(Y, Z)))
proof
let X,Y,Z,D be set;
assume
A1: D c= Funcs([:X,Y:], Z);
per cases;
suppose
D is empty;
then reconsider F={} as ManySortedSet of D by PARTFUN1:def 2,RELAT_1:38
,def 18;
take F;
thus F is currying;
assume Y = {} implies X = {};
thus thesis;
end;
suppose
D is non empty;
then reconsider E=D as non empty functional set by A1;
deffunc F(Function) = curry $1;
consider F being ManySortedSet of E such that
A2: for d being Element of E holds F.d = F(d) from PBOOLE:sch 5;
reconsider F1=F as ManySortedSet of D;
take F1;
thus F1 is currying
proof
hereby
let x be set;
assume x in dom F1;
then
A3: x in D;
hence x is Function by A1;
ex x1 being Function st x1=x & dom x1=[:X,Y:] &
rng x1 c= Z by A3,A1,FUNCT_2:def 2;
hence proj1 x is Relation;
end;
let f be Function;
assume f in dom F1;
then reconsider d=f as Element of E;
thus F1.f = F.d .= curry f by A2;
end;
assume
A4: Y = {} implies X = {};
thus rng F1 c= Funcs(X, Funcs(Y, Z))
proof
let y be object;
assume y in rng F1;
then consider x being object such that
A5: x in dom F1 and
A6: y = F1.x by FUNCT_1:def 3;
reconsider d=x as Element of E by A5;
A7: y = curry d by A2,A6;
A8: d in Funcs([:X,Y:], Z) by A1;
per cases;
suppose
A9: [:X,Y:] = {};
then
A10: d is Function of {}, Z by A8,FUNCT_2:66;
now
assume
A11: X = {};
then y is Function of X, Funcs(Y,Z) by A7,A10,FUNCT_5:42,RELSET_1:12;
hence thesis by A11,FUNCT_2:8;
end;
hence thesis by A4,A9;
end;
suppose
[:X,Y:] <> {};
hence thesis by A7,A8,FUNCT_6:10;
end;
end;
end;
end;
registration
let X,Y,Z be set;
cluster uncurrying for ManySortedSet of Funcs(X, Funcs(Y, Z));
existence
proof
ex F being ManySortedSet of Funcs(X, Funcs(Y, Z)) st F is uncurrying &
rng F c= Funcs([:X,Y:], Z) by Th1;
hence thesis;
end;
cluster currying for ManySortedSet of Funcs([:X, Y:], Z);
existence
proof
ex F being ManySortedSet of Funcs([:X, Y:], Z) st F is currying & ((Y
= {} implies X = {}) implies rng F c= Funcs(X, Funcs(Y, Z))) by Th2;
hence thesis;
end;
end;
theorem Th3:
for A,B being non empty set, 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
let A,B be non empty set;
let C be set;
let f,g be commuting Function;
assume that
A1: dom f c= Funcs(A, Funcs(B, C)) and
A2: rng f c= dom g;
A3: now
let x be object;
assume
A4: x in dom f;
then reconsider X=x as Function by Def3;
A5: f.x in rng f by A4,FUNCT_1:def 3;
then reconsider Y=f.x as Function by A2,Def3;
thus (g*f).x = g.(f.x) by A4,FUNCT_1:13
.= commute Y by A2,A5,Def3
.= commute (commute X) by A4,Def3
.= x by A1,A4,FUNCT_6:57;
end;
dom (g*f) = dom f by A2,RELAT_1:27;
hence thesis by A3,FUNCT_1:17;
end;
theorem Th4:
for B being non empty set, 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
let B be non empty set;
let A,C be set;
let f be uncurrying Function;
let g be currying Function;
assume that
A1: dom f c= Funcs(A, Funcs(B, C)) and
A2: rng f c= dom g;
A3: now
let x be object;
assume
A4: x in dom f;
then reconsider X=x as Function by Def1;
A5: ex F being Function st X = F & dom F = A & rng F c=
Funcs(B, C) by A1,A4,FUNCT_2:def 2;
A6: f.x in rng f by A4,FUNCT_1:def 3;
then reconsider Y=f.x as Function by A2,Def2;
thus (g*f).x = g.(f.x) by A4,FUNCT_1:13
.= curry Y by A2,A6,Def2
.= curry (uncurry X) by A4,Def1
.= x by A5,FUNCT_5:48;
end;
dom (g*f) = dom f by A2,RELAT_1:27;
hence thesis by A3,FUNCT_1:17;
end;
theorem Th5:
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
let A,B,C be set;
let f be currying Function;
let g be uncurrying Function;
assume that
A1: dom f c= Funcs([:A, B:], C) and
A2: rng f c= dom g;
A3: now
let x be object;
assume
A4: x in dom f;
then reconsider X=x as Function by Def2;
A5: ex F being Function st X = F & dom F = [:A, B:] & rng
F c= C by A1,A4,FUNCT_2:def 2;
A6: f.x in rng f by A4,FUNCT_1:def 3;
then reconsider Y=f.x as Function by A2,Def1;
thus (g*f).x = g.(f.x) by A4,FUNCT_1:13
.= uncurry Y by A2,A6,Def1
.= uncurry (curry X) by A4,Def2
.= x by A5,FUNCT_5:49;
end;
dom (g*f) = dom f by A2,RELAT_1:27;
hence thesis by A3,FUNCT_1:17;
end;
theorem Th6:
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
let f be Function-yielding Function;
let i,A be set;
A1: commute f = curry' uncurry f by FUNCT_6:def 10
.= curry ~(uncurry f) by FUNCT_5:def 3;
assume
A2: i in dom commute f;
thus ((commute f).i).:A c= pi(f.:A, i)
proof
let x be object;
assume x in ((commute f).i).:A;
then consider y being object such that
A3: y in dom ((commute f).i) and
A4: y in A and
A5: x = ((commute f).i).y by FUNCT_1:def 6;
A6: [i,y] in dom ~(uncurry f) by A2,A1,A3,FUNCT_5:31;
then
A7: [y,i] in dom uncurry f by FUNCT_4:42;
then ex a being object,g being Function, b being object st [y,i] =
[a,b] & a in dom f & g = f.a & b in dom g by FUNCT_5:def 2;
then y in dom f by XTUPLE_0:1;
then
A8: f.y in f.:A by A4,FUNCT_1:def 6;
A9: [y,i]`2=i;
A10: [y,i]`1=y;
x = ~(uncurry f).(i,y) by A2,A1,A3,A5,FUNCT_5:31
.= (uncurry f).(y,i) by A6,FUNCT_4:43
.= (f.y qua Function).i by A7,A10,A9,FUNCT_5:def 2;
hence thesis by A8,CARD_3:def 6;
end;
end;
theorem Th7:
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
let f be Function-yielding Function;
let i,A be set;
assume
A1: for g being Function st g in f.:A holds i in dom g;
let x be object;
assume x in pi(f.:A, i);
then consider g being Function such that
A2: g in f.:A and
A3: x = g.i by CARD_3:def 6;
consider y being object such that
A4: y in dom f and
A5: y in A and
A6: g = f.y by A2,FUNCT_1:def 6;
i in dom g by A1,A2;
then
A7: [y,i] in dom uncurry f by A4,A6,FUNCT_5:def 2;
then
A8: [i,y] in dom ~(uncurry f) by FUNCT_4:def 2;
then
A9: i in proj1 dom ~(uncurry f) by XTUPLE_0:def 12;
then
A10: i in dom curry ~(uncurry f) by FUNCT_5:def 1;
A11: i in {i} by TARSKI:def 1;
y in proj2 dom ~(uncurry f) by A8,XTUPLE_0:def 13;
then [i,y] in [:{i},proj2 dom ~(uncurry f):] by A11,ZFMISC_1:87;
then
A12: [i,y]in(dom ~(uncurry f) /\ [:{i},proj2 dom ~(uncurry f):]) by A8,
XBOOLE_0:def 4;
then
A13: y in proj2 (dom ~(uncurry f) /\ [:{i},proj2 dom ~(uncurry f):]) by
XTUPLE_0:def 13;
A14: [y,i]`2=i;
A15: [y,i]`1=y;
A16: commute f = curry' uncurry f by FUNCT_6:def 10
.= curry ~(uncurry f) by FUNCT_5:def 3;
A17: ex h being Function st (curry ~(uncurry f)).i = h & dom
h = proj2 (dom ~(uncurry f) /\ [:{i},proj2 dom ~(uncurry f):]) &
for b being object st b in dom h holds h.b = (~(uncurry f)).(i,b)
by A9,FUNCT_5:def 1;
then y in dom ((commute f).i) by A16,A12,XTUPLE_0:def 13;
then ((commute f).i).y = ~(uncurry f).(i,y) by A16,A10,FUNCT_5:31
.= (uncurry f).(y,i) by A7,FUNCT_4:def 2
.= x by A3,A6,A7,A15,A14,FUNCT_5:def 2;
hence thesis by A5,A16,A17,A13,FUNCT_1:def 6;
end;
theorem Th8:
for X,Y being set, f being Function st rng f c= Funcs(X, Y) for i
,A being set st i in X holds ((commute f).i).:A = pi(f.:A, i)
proof
let X,Y be set, f be Function;
assume
A1: rng f c= Funcs(X, Y);
then
A2: f in Funcs(dom f, Funcs(X, Y)) by FUNCT_2:def 2;
A3: f is Function-yielding
proof
let x be object;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A1;
end;
let i, A be set;
assume
A4: i in X;
per cases;
suppose
dom f = {};
then
A5: f = {};
then (commute f).i = {} by FUNCT_6:58;
then
A6: ((commute f).i).:A = {};
f.:A = {} by A5;
hence thesis by A6,CARD_3:13;
end;
suppose
dom f <> {};
then commute f in Funcs(X, Funcs(dom f, Y)) by A2,A4,FUNCT_6:55;
then
ex g being Function st commute f = g & dom g = X & rng g c= Funcs(dom
f, Y) by FUNCT_2:def 2;
hence ((commute f).i).:A c= pi(f.:A, i) by A3,A4,Th6;
now
let g be Function;
A7: f.:A c= rng f by RELAT_1:111;
assume g in f.:A;
then g in rng f by A7;
then ex h being Function st g = h & dom h = X & rng h c= Y by A1,
FUNCT_2:def 2;
hence i in dom g by A4;
end;
hence thesis by A3,Th7;
end;
end;
theorem Th9:
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
let f be Function, i, A be set such that
A1: [:A,{i}:] c= dom f;
A2: i in {i} by TARSKI:def 1;
thus pi((curry f).:A, i) c= f.:[:A,{i}:]
proof
let x be object;
assume x in pi((curry f).:A, i);
then consider g being Function such that
A3: g in (curry f).:A and
A4: x = g.i by CARD_3:def 6;
consider a being object such that
a in dom curry f and
A5: a in A and
A6: g = (curry f).a by A3,FUNCT_1:def 6;
A7: [a,i] in [:A, {i}:] by A2,A5,ZFMISC_1:def 2;
then f.(a,i) in f.:[:A, {i}:] by A1,FUNCT_1:def 6;
hence thesis by A1,A4,A6,A7,FUNCT_5:20;
end;
let x be object;
assume x in f.:[:A,{i}:];
then consider y being object such that
A8: y in dom f and
A9: y in [:A, {i}:] and
A10: x = f.y by FUNCT_1:def 6;
consider y1,y2 being object such that
A11: y1 in A and
A12: y2 in {i} and
A13: y = [y1,y2] by A9,ZFMISC_1:def 2;
reconsider g = (curry f).y1 as Function;
y1 in dom curry f by A8,A13,FUNCT_5:19;
then
A14: g in (curry f).:A by A11,FUNCT_1:def 6;
A15: y2 = i by A12,TARSKI:def 1;
x = f.(y1,y2) by A10,A13;
then x = g.i by A15,A8,A13,FUNCT_5:20;
hence thesis by A14,CARD_3:def 6;
end;
registration
let T be constituted-Functions 1-sorted;
cluster the carrier of T -> functional;
coherence;
end;
registration
cluster constituted-Functions complete strict for LATTICE;
existence
proof
set L = the complete LATTICE;
take L|^{};
thus thesis;
end;
cluster constituted-Functions non empty for 1-sorted;
existence
proof
set L = the complete LATTICE;
take L|^{};
thus thesis;
end;
end;
registration
let T be constituted-Functions non empty RelStr;
cluster -> constituted-Functions for non empty SubRelStr of T;
coherence
proof
let S be non empty SubRelStr of T;
let a be Element of S;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
hence thesis;
end;
end;
theorem Th10:
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
let S,T be complete LATTICE;
let f be idempotent Function of T,T;
let h be Function of S, Image f;
rng h c= the carrier of Image f;
then
A1: rng h c= rng f by YELLOW_0:def 15;
f*f = f by QUANTAL1:def 9;
then rng f c= dom f by FUNCT_1:15;
then rng h c= dom f by A1;
hence thesis by A1,YELLOW16:4;
end;
theorem
for S being non empty RelStr for T,T1 being non empty RelStr st T is
SubRelStr of T1 for f being Function of S, T for f1 being Function of S, T1
holds f is monotone & f=f1 implies f1 is monotone
proof
let S be non empty RelStr;
let T,T1 be non empty RelStr;
assume
A1: T is SubRelStr of T1;
let f be Function of S, T;
let f1 be Function of S, T1;
assume that
A2: f is monotone and
A3: f=f1;
thus f1 is monotone
proof
let x,y be Element of S;
assume x <= y;
then f.x <= f.y by A2;
hence thesis by A1,A3,YELLOW_0:59;
end;
end;
theorem Th12:
for S being non empty RelStr for T,T1 being non empty RelStr st
T is full SubRelStr of T1 for f being Function of S, T for f1 being Function of
S, T1 holds f1 is monotone & f=f1 implies f is monotone
proof
let S be non empty RelStr;
let T,T1 be non empty RelStr;
assume
A1: T is full SubRelStr of T1;
let f be Function of S, T;
let f1 be Function of S, T1;
assume that
A2: f1 is monotone and
A3: f=f1;
thus f is monotone
proof
let x,y be Element of S;
assume x <= y;
then f1.x <= f1.y by A2;
hence thesis by A1,A3,YELLOW_0:60;
end;
end;
theorem Th13:
for X being set, V being Subset of X holds chi(V,X)"{1} = V &
chi(V,X)"{0} = X\V
proof
let X be set;
let V be Subset of X;
thus chi(V,X)"{1} = V
proof
thus chi(V,X)"{1} c= V
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A1: x in chi(V,X)"{1};
then chi(V,X).x in {1} by FUNCT_1:def 7;
then
chi(V,X).xx = {0} by TARSKI:def 1,CARD_1:49;
then chi(V,X).xx <> {};
hence thesis by A1,FUNCT_3:def 3;
end;
let x be object;
assume
A2: x in V;
then chi(V,X).x = 1 by FUNCT_3:def 3;
then
A3: chi(V,X).x in {1} by TARSKI:def 1;
x in X by A2;
then x in dom chi(V,X) by FUNCT_3:def 3;
hence thesis by A3,FUNCT_1:def 7;
end;
thus chi(V,X)"{0} = X\V
proof
thus chi(V,X)"{0} c= X\V
proof
let x be object;
A4: x in V implies chi(V,X).x = 1 by FUNCT_3:def 3;
assume
A5: x in chi(V,X)"{0};
then chi(V,X).x in {0} by FUNCT_1:def 7;
hence thesis by A4,A5,TARSKI:def 1,XBOOLE_0:def 5;
end;
let x be object;
assume
A6: x in X\V;
then not x in V by XBOOLE_0:def 5;
then chi(V,X).x = 0 by A6,FUNCT_3:def 3;
then
A7: chi(V,X).x in {0} by TARSKI:def 1;
x in X by A6;
then x in dom chi(V,X) by FUNCT_3:def 3;
hence thesis by A7,FUNCT_1:def 7;
end;
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;
redefine func f.x -> Element of T; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider p = f as Element of product (X --> T) by YELLOW_1:def 5;
p.x is Element of (X --> T).x;
hence thesis;
end;
end;
theorem Th14:
for X being non empty set, 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
let X be non empty set, T be non empty RelStr;
let f,g be Element of T|^X;
reconsider a = f, b = g as Element of product (X --> T) by YELLOW_1:def 5;
A1: T|^X = product (X --> T) by YELLOW_1:def 5;
hereby
assume
A2: f <= g;
let x be Element of X;
(X --> T).x = T;
hence f.x <= g.x by A1,A2,WAYBEL_3:28;
end;
assume for x being Element of X holds f.x <= g.x;
then for x be Element of X holds a.x <= b.x;
hence thesis by A1,WAYBEL_3:28;
end;
theorem Th15:
for X being set for L,S being non empty RelStr st the RelStr of
L = the RelStr of S holds L|^X = S|^X
proof
let X be set;
let L,S be non empty RelStr such that
A1: the RelStr of L = the RelStr of S;
reconsider tXL = (X)--> L as RelStr-yielding ManySortedSet of X;
reconsider tXS = (X)--> S as RelStr-yielding ManySortedSet of X;
A2: for x being object st x in dom (Carrier tXS) holds (Carrier tXS).x = (
Carrier tXL).x
proof
let x be object;
assume x in dom (Carrier tXS);
then
A3: x in X;
then
A4: ex R1 being 1-sorted st tXL.x = R1 & (Carrier tXL).x =
the carrier of R1 by PRALG_1:def 15;
ex R being 1-sorted st tXS.x = R & (Carrier tXS).x =
the carrier of R by A3,PRALG_1:def 15;
hence (Carrier tXS).x = the carrier of S by A3,FUNCOP_1:7
.= (Carrier tXL).x by A1,A3,A4,FUNCOP_1:7;
end;
A5: dom (Carrier tXS) = X by PARTFUN1:def 2
.= dom (Carrier tXL) by PARTFUN1:def 2;
A6: the carrier of S|^X = the carrier of product tXS by YELLOW_1:def 5
.= product Carrier tXS by YELLOW_1:def 4
.= product Carrier tXL by A5,A2,FUNCT_1:2
.= the carrier of product tXL by YELLOW_1:def 4
.= the carrier of L|^X by YELLOW_1:def 5;
A7: the InternalRel of L|^X c= the InternalRel of S|^X
proof
reconsider tXS=(X) --> S as RelStr-yielding ManySortedSet of X;
reconsider tXL=(X) --> L as RelStr-yielding ManySortedSet of X;
let x be object;
assume
A8: x in the InternalRel of L|^X;
then consider a,b being object such that
A9: x = [a,b] and
A10: a in the carrier of L|^X and
A11: b in the carrier of L|^X by RELSET_1:2;
reconsider a,b as Element of L|^X by A10,A11;
A12: L|^X = product tXL by YELLOW_1:def 5;
then
A13: the carrier of L|^X=product Carrier tXL by YELLOW_1:def 4;
a <= b by A8,A9,ORDERS_2:def 5;
then consider f,g being Function such that
A14: f = a and
A15: g = b and
A16: for i be object st i in X ex R being RelStr, xi,yi being Element of
R st R = tXL.i & xi = f.i & yi = g.i & xi <= yi by A12,A13,YELLOW_1:def 4;
reconsider a1=a,b1=b as Element of S|^X by A6;
A17: ex f,g being Function st f = a1 & g = b1 &
for i be object st i in X ex
R being RelStr, xi,yi being Element of R st R = tXS.i & xi = f.i & yi = g.i &
xi <= yi
proof
take f,g;
thus f=a1 & g=b1 by A14,A15;
let i be object;
assume
A18: i in X;
then consider R being RelStr, xi,yi being Element of R such that
A19: R = tXL.i and
A20: xi = f.i and
A21: yi = g.i and
A22: xi <= yi by A16;
take R1=S;
reconsider xi1=xi,yi1=yi as Element of R1 by A1,A18,A19,FUNCOP_1:7;
take xi1,yi1;
thus R1=tXS.i by A18,FUNCOP_1:7;
thus xi1 = f.i & yi1 = g.i by A20,A21;
the InternalRel of R = the InternalRel of L by A18,A19,FUNCOP_1:7;
then [xi1,yi1] in the InternalRel of R1 by A1,A22,ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
A23: S|^X = product tXS by YELLOW_1:def 5;
then the carrier of S|^X=product Carrier tXS by YELLOW_1:def 4;
then a1 <= b1 by A17,A23,YELLOW_1:def 4;
hence thesis by A9,ORDERS_2:def 5;
end;
the InternalRel of S|^X c= the InternalRel of L|^X
proof
reconsider tXL=(X) --> L as RelStr-yielding ManySortedSet of X;
reconsider tXS=(X) --> S as RelStr-yielding ManySortedSet of X;
let x be object;
assume
A24: x in the InternalRel of S|^X;
then consider a,b being object such that
A25: x = [a,b] and
A26: a in the carrier of S|^X and
A27: b in the carrier of S|^X by RELSET_1:2;
reconsider a,b as Element of S|^X by A26,A27;
A28: S|^X = product tXS by YELLOW_1:def 5;
then
A29: the carrier of S|^X=product Carrier tXS by YELLOW_1:def 4;
a <= b by A24,A25,ORDERS_2:def 5;
then consider f,g being Function such that
A30: f = a and
A31: g = b and
A32: for i be object st i in X ex R being RelStr, xi,yi being Element of
R st R = tXS.i & xi = f.i & yi = g.i & xi <= yi by A28,A29,YELLOW_1:def 4;
reconsider a1=a,b1=b as Element of L|^X by A6;
A33: ex f,g being Function st f = a1 & g = b1 &
for i be object st i in X ex
R being RelStr, xi,yi being Element of R st R = tXL.i & xi = f.i & yi = g.i &
xi <= yi
proof
take f,g;
thus f=a1 & g=b1 by A30,A31;
let i be object;
assume
A34: i in X;
then consider R being RelStr, xi,yi being Element of R such that
A35: R = tXS.i and
A36: xi = f.i and
A37: yi = g.i and
A38: xi <= yi by A32;
take R1=L;
reconsider xi1=xi,yi1=yi as Element of R1 by A1,A34,A35,FUNCOP_1:7;
take xi1,yi1;
thus R1=tXL.i by A34,FUNCOP_1:7;
thus xi1 = f.i & yi1 = g.i by A36,A37;
the InternalRel of R = the InternalRel of S by A34,A35,FUNCOP_1:7;
then [xi1,yi1] in the InternalRel of R1 by A1,A38,ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
A39: L|^X = product tXL by YELLOW_1:def 5;
then the carrier of L|^X=product Carrier tXL by YELLOW_1:def 4;
then a1 <= b1 by A33,A39,YELLOW_1:def 4;
hence thesis by A25,ORDERS_2:def 5;
end;
hence thesis by A7,A6,XBOOLE_0:def 10;
end;
theorem
for S1,S2,T1,T2 being non empty TopSpace st the TopStruct of S1 = the
TopStruct of S2 & the TopStruct of T1 = the TopStruct of T2 holds oContMaps(S1,
T1) = oContMaps(S2, T2)
proof
let S1,S2,T1,T2 be non empty TopSpace;
assume that
A1: the TopStruct of S1 = the TopStruct of S2 and
A2: the TopStruct of T1 = the TopStruct of T2;
A3: oContMaps(S2, T2) = ContMaps(S2, Omega T2) by WAYBEL26:def 1;
Omega T1 = Omega T2 by A2,WAYBEL25:13;
then reconsider
oCM2 = oContMaps(S2, T2) as full SubRelStr of (Omega T1) |^ the
carrier of S1 by A3,A1,WAYBEL24:def 3;
oContMaps(S1, T1) = ContMaps(S1, Omega T1) by WAYBEL26:def 1;
then reconsider
oCM1 = oContMaps(S1, T1) as full SubRelStr of (Omega T1) |^ the
carrier of S1 by WAYBEL24:def 3;
the carrier of oCM1 = the carrier of oCM2
proof
thus the carrier of oCM1 c= the carrier of oCM2
proof
let x be object;
A4: the TopStruct of Omega T2 = the TopStruct of T2 by WAYBEL25:def 2;
assume x in the carrier of oCM1;
then x in the carrier of ContMaps(S1, Omega T1) by WAYBEL26:def 1;
then consider f being Function of S1, Omega T1 such that
A5: x = f and
A6: f is continuous by WAYBEL24:def 3;
A7: the TopStruct of Omega T1 = the TopStruct of T1 by WAYBEL25:def 2;
then reconsider f1=f as Function of S2, Omega T2 by A4,A1,A2;
for P1 being Subset of Omega T2 st P1 is closed holds f1" P1 is closed
proof
let P1 be Subset of Omega T2;
reconsider P = P1 as Subset of (Omega T1) by A2,A7,A4;
assume P1 is closed;
then P is closed by A2,A7,A4,TOPS_3:79;
then f"P is closed by A6,PRE_TOPC:def 6;
hence thesis by A1,TOPS_3:79;
end;
then f1 is continuous by PRE_TOPC:def 6;
then x in the carrier of ContMaps(S2, Omega T2) by A5,WAYBEL24:def 3;
hence thesis by WAYBEL26:def 1;
end;
let x be object;
A8: the TopStruct of Omega T1 = the TopStruct of T1 by WAYBEL25:def 2;
assume x in the carrier of oCM2;
then x in the carrier of ContMaps(S2, Omega T2) by WAYBEL26:def 1;
then consider f being Function of S2, Omega T2 such that
A9: x = f and
A10: f is continuous by WAYBEL24:def 3;
A11: the TopStruct of Omega T2 = the TopStruct of T2 by WAYBEL25:def 2;
then reconsider f1=f as Function of S1, Omega T1 by A8,A1,A2;
for P1 being Subset of Omega T1 st P1 is closed holds f1" P1 is closed
proof
let P1 be Subset of Omega T1;
reconsider P = P1 as Subset of (Omega T2) by A2,A11,A8;
assume P1 is closed;
then P is closed by A2,A11,A8,TOPS_3:79;
then f"P is closed by A10,PRE_TOPC:def 6;
hence thesis by A1,TOPS_3:79;
end;
then f1 is continuous by PRE_TOPC:def 6;
then x in the carrier of ContMaps(S1, Omega T1) by A9,WAYBEL24:def 3;
hence thesis by WAYBEL26:def 1;
end;
hence thesis by YELLOW_0:57;
end;
theorem Th17:
for X being set ex f being Function of BoolePoset X, (BoolePoset
{0})|^X st f is isomorphic & for Y being Subset of X holds f.Y = chi(Y,X)
proof
let Z be set;
per cases;
suppose
A1: Z = {};
then
A2: (BoolePoset{0})|^Z = RelStr(#{{}}, id {{}}#) by YELLOW_1:27;
A3: InclPoset bool {} = RelStr(#bool {}, RelIncl bool {}#) by YELLOW_1:def 1;
A4: BoolePoset Z = InclPoset bool {} by A1,YELLOW_1:4;
then reconsider
f = id {{}} as Function of BoolePoset Z, (BoolePoset{0})|^Z by A3,A1,
YELLOW_1:27,ZFMISC_1:1;
take f;
A5: rng id {{}} = {{}};
for x,y being Element of BoolePoset Z holds x <= y iff f.x <= f.y by A4,A3;
hence f is isomorphic by A2,A5,WAYBEL_0:66;
let Y be Subset of Z;
Y = {} by A1;
then Y in {{}} by TARSKI:def 1;
then f.Y = {} by A1,FUNCT_1:18;
hence thesis by A1;
end;
suppose
Z <> {};
then reconsider Z9 = Z as non empty set;
(BoolePoset{0})|^Z = product (Z9 --> BoolePoset{0}) by YELLOW_1:def 5;
hence thesis by WAYBEL18:14;
end;
end;
theorem Th18:
for X being set holds BoolePoset X, (BoolePoset{0})|^X are_isomorphic
proof
let X be set;
consider f being Function of BoolePoset X, (BoolePoset{0})|^X such that
A1: f is isomorphic and
for Y being Subset of X holds f.Y = chi(Y,X) by Th17;
take f;
thus thesis by A1;
end;
theorem Th19:
for X,Y being non empty set, T being non empty Poset for S1
being full non empty SubRelStr of (T|^X)|^Y for S2 being full non empty
SubRelStr of (T|^Y)|^X for F being Function of S1, S2 st F is commuting holds F
is monotone
proof
let X,Y be non empty set, T be non empty Poset;
let S1 be full non empty SubRelStr of (T|^X)|^Y;
let S2 be full non empty SubRelStr of (T|^Y)|^X;
let F be Function of S1, S2 such that
for x being set st x in dom F holds x is Function-yielding Function and
A1: for f being Function st f in dom F holds F.f = commute f;
let f,g be Element of S1;
A2: dom F = the carrier of S1 by FUNCT_2:def 1;
then
A3: F.g = commute g by A1;
reconsider Fa = F.f, Fb = F.g as Element of (T|^Y)|^X by YELLOW_0:58;
reconsider a = f, b = g as Element of (T|^X)|^Y by YELLOW_0:58;
A4: the carrier of (T|^X)|^Y = Funcs(Y, the carrier of T|^X) by YELLOW_1:28
.= Funcs(Y, Funcs(X, the carrier of T)) by YELLOW_1:28;
assume f <= g;
then
A5: a <= b by YELLOW_0:59;
A6: F.f = commute a by A2,A1;
now
let x be Element of X;
now
let y be Element of Y;
A7: Fa.x.y = a.y.x by A4,A6,FUNCT_6:56;
A8: Fb.x.y = b.y.x by A4,A3,FUNCT_6:56;
a.y <= b.y by A5,Th14;
hence Fa.x.y <= Fb.x.y by A7,A8,Th14;
end;
hence Fa.x <= Fb.x by Th14;
end;
then Fa <= Fb by Th14;
hence thesis by YELLOW_0:60;
end;
theorem Th20:
for X,Y being non empty set, T being non empty Poset for S1
being full non empty SubRelStr of (T|^Y)|^X for S2 being full non empty
SubRelStr of T|^[:X,Y:] for F being Function of S1, S2 st F is uncurrying holds
F is monotone
proof
let X,Y be non empty set, T be non empty Poset;
let S1 be full non empty SubRelStr of (T|^Y)|^X;
let S2 be full non empty SubRelStr of T|^[:X,Y:];
let F be Function of S1, S2 such that
for x being set st x in dom F holds x is Function-yielding Function and
A1: for f being Function st f in dom F holds F.f = uncurry f;
let f,g be Element of S1;
reconsider a = f, b = g as Element of (T|^Y)|^X by YELLOW_0:58;
A2: dom F = the carrier of S1 by FUNCT_2:def 1;
then
A3: F.g = uncurry b by A1;
reconsider Fa = F.f, Fb = F.g as Element of T|^[:X,Y:] by YELLOW_0:58;
assume f <= g;
then
A4: a <= b by YELLOW_0:59;
A5: the carrier of T|^Y = Funcs(Y, the carrier of T) by YELLOW_1:28;
then
A6: the carrier of (T|^Y)|^X = Funcs(X, Funcs(Y, the carrier of T)) by
YELLOW_1:28;
A7: F.f = uncurry a by A2,A1;
now
let xy be Element of [:X,Y:];
consider x,y being object such that
A8: x in X and
A9: y in Y and
A10: xy = [x,y] by ZFMISC_1:def 2;
reconsider y as Element of Y by A9;
reconsider x as Element of X by A8;
A11: a.x <= b.x by A4,Th14;
b is Function of X, Funcs(Y, the carrier of T) by A6,FUNCT_2:66;
then
A12: dom b = X by FUNCT_2:def 1;
a is Function of X, Funcs(Y, the carrier of T) by A6,FUNCT_2:66;
then
A13: dom a = X by FUNCT_2:def 1;
b.x is Function of Y, the carrier of T by A5,FUNCT_2:66;
then dom (b.x) = Y by FUNCT_2:def 1;
then
A14: Fb.(x,y) = b.x.y by A12,A3,FUNCT_5:38;
a.x is Function of Y, the carrier of T by A5,FUNCT_2:66;
then dom (a.x) = Y by FUNCT_2:def 1;
then Fa.(x,y) = a.x.y by A13,A7,FUNCT_5:38;
hence Fa.xy <= Fb.xy by A14,A11,A10,Th14;
end;
then Fa <= Fb by Th14;
hence thesis by YELLOW_0:60;
end;
theorem Th21:
for X,Y being non empty set, T being non empty Poset for S1
being full non empty SubRelStr of (T|^Y)|^X for S2 being full non empty
SubRelStr of T|^[:X,Y:] for F being Function of S2, S1 st F is currying holds F
is monotone
proof
let X,Y be non empty set, T be non empty Poset;
let S1 be full non empty SubRelStr of (T|^Y)|^X;
let S2 be full non empty SubRelStr of T|^[:X,Y:];
let F be Function of S2, S1 such that
for x being set st x in dom F holds x is Function & proj1 x is Relation and
A1: for f being Function st f in dom F holds F.f = curry f;
let f,g be Element of S2;
reconsider a = f, b = g as Element of T|^[:X,Y:] by YELLOW_0:58;
A2: dom F = the carrier of S2 by FUNCT_2:def 1;
then
A3: F.g = curry b by A1;
reconsider Fa = F.f, Fb = F.g as Element of (T|^Y)|^X by YELLOW_0:58;
assume f <= g;
then
A4: a <= b by YELLOW_0:59;
A5: the carrier of T|^Y = Funcs(Y, the carrier of T) by YELLOW_1:28;
then
A6: the carrier of (T|^Y)|^X = Funcs(X, Funcs(Y, the carrier of T)) by
YELLOW_1:28;
A7: F.f = curry a by A2,A1;
now
let x be Element of X;
now
let y be Element of Y;
reconsider xy = [x,y] as Element of [:X,Y:];
Fa.x is Function of Y, the carrier of T by A5,FUNCT_2:66;
then
A8: dom (Fa.x) = Y by FUNCT_2:def 1;
Fa is Function of X, Funcs(Y, the carrier of T) by A6,FUNCT_2:66;
then dom Fa = X by FUNCT_2:def 1;
then Fa.x.y = a.(x,y) by A8,A7,FUNCT_5:31;
then
A9: Fa.x.y = a.xy;
Fb.x is Function of Y, the carrier of T by A5,FUNCT_2:66;
then
A10: dom (Fb.x) = Y by FUNCT_2:def 1;
Fb is Function of X, Funcs(Y, the carrier of T) by A6,FUNCT_2:66;
then dom Fb = X by FUNCT_2:def 1;
then Fb.x.y = b.(x,y) by A10,A3,FUNCT_5:31;
hence Fa.x.y <= Fb.x.y by A9,A4,Th14;
end;
hence Fa.x <= Fb.x by Th14;
end;
then Fa <= Fb by Th14;
hence thesis by YELLOW_0:60;
end;
begin :: Again poset of continuous maps
definition
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
func UPS(S, T) -> strict RelStr means
: Def4:
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
defpred P[object] means $1 is directed-sups-preserving Function of S, T;
consider X be set such that
A1: for a be object holds a in X iff a in the carrier of (T |^ the
carrier of S) & P[a] from XBOOLE_0:sch 1;
X c= the carrier of T |^ the carrier of S
by A1;
then reconsider X as Subset of (T |^ the carrier of S);
take SX = subrelstr X;
thus SX is full SubRelStr of T |^ the carrier of S;
let f be set;
thus f in the carrier of SX implies f is directed-sups-preserving Function
of S,T
proof
assume f in the carrier of SX;
then f in X by YELLOW_0:def 15;
hence thesis by A1;
end;
assume
A2: f is directed-sups-preserving Function of S,T;
then f is Element of T |^ the carrier of S by WAYBEL24:19;
then f in X by A1,A2;
hence thesis by YELLOW_0:def 15;
end;
uniqueness
proof
let U1,U2 be strict RelStr;
assume that
A3: U1 is full SubRelStr of T |^ the carrier of S and
A4: for x being set holds x in the carrier of U1 iff x is
directed-sups-preserving Function of S, T and
A5: U2 is full SubRelStr of T |^ the carrier of S and
A6: for x being set holds x in the carrier of U2 iff x is
directed-sups-preserving Function of S, T;
the carrier of U1 = the carrier of U2
proof
hereby
let x be object;
assume x in the carrier of U1;
then x is directed-sups-preserving Function of S, T by A4;
hence x in the carrier of U2 by A6;
end;
let x be object;
assume x in the carrier of U2;
then x is directed-sups-preserving Function of S, T by A6;
hence thesis by A4;
end;
hence thesis by A3,A5,YELLOW_0:57;
end;
end;
registration
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
cluster UPS(S, T) -> non empty reflexive antisymmetric constituted-Functions;
coherence
proof
set f = the directed-sups-preserving Function of S, T;
f in the carrier of UPS(S, T) by Def4;
then UPS(S, T) is full non empty SubRelStr of T |^ the carrier of S by Def4
;
hence thesis;
end;
end;
registration
let S be non empty RelStr;
let T be non empty Poset;
cluster UPS(S,T) -> transitive;
coherence
proof
UPS(S,T) is full SubRelStr of T |^ the carrier of S by Def4;
hence thesis;
end;
end;
theorem Th22:
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
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
UPS(S, T) is SubRelStr of T|^the carrier of S by Def4;
then the carrier of UPS(S, T) c= the carrier of T|^the carrier of S by
YELLOW_0:def 13;
hence thesis by YELLOW_1:28;
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;
redefine func f.s -> Element of T; :: redefines . (FUNCT_1, definition)
coherence
proof
UPS(S, T) is SubRelStr of T|^the carrier of S by Def4;
then reconsider p = f as Element of T|^the carrier of S by YELLOW_0:58;
p.s = p.s;
hence thesis;
end;
end;
theorem Th23:
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
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
let f,g be Element of UPS(S, T);
A1: UPS(S, T) is full SubRelStr of T|^the carrier of S by Def4;
then reconsider a = f, b = g as Element of T|^the carrier of S by YELLOW_0:58
;
A2: f <= g iff a <= b by A1,YELLOW_0:59,60;
hence f <= g implies for s being Element of S holds f.s <= g.s by Th14;
assume for s being Element of S holds f.s <= g.s;
hence thesis by A2,Th14;
end;
theorem Th24:
for S,T being complete Scott TopLattice holds UPS(S,T) = SCMaps( S,T)
proof
let S,T be complete Scott TopLattice;
A1: the carrier of UPS(S,T) = the carrier of SCMaps(S,T)
proof
thus the carrier of UPS(S,T) c= the carrier of SCMaps(S,T)
proof
let x be object;
assume x in the carrier of UPS(S,T);
then reconsider f=x as directed-sups-preserving Function of S,T by Def4;
f is continuous;
hence thesis by WAYBEL17:def 2;
end;
let x be object;
assume
A2: x in the carrier of SCMaps(S,T);
the carrier of SCMaps(S,T) c= the carrier of MonMaps(S,T) by
YELLOW_0:def 13;
then reconsider f=x as Function of S,T by A2,WAYBEL10:9;
f is continuous by A2,WAYBEL17:def 2;
hence thesis by Def4;
end;
then
A3: the carrier of UPS(S,T) c= the carrier of MonMaps(S,T) by YELLOW_0:def 13;
UPS(S,T) is full SubRelStr of T |^ the carrier of S by Def4;
then the InternalRel of UPS(S,T) = (the InternalRel of (T |^ the carrier of
S)) |_2 the carrier of UPS(S,T) by YELLOW_0:def 14
.=((the InternalRel of (T |^ the carrier of S)) |_2 the carrier of
MonMaps(S,T)) |_2 the carrier of UPS(S,T) by A3,WELLORD1:22
.=(the InternalRel of MonMaps(S,T)) |_2 the carrier of SCMaps(S,T) by A1,
YELLOW_0:def 14
.= the InternalRel of SCMaps(S,T) by YELLOW_0:def 14;
hence thesis by A1;
end;
theorem Th25:
for S,S9 being non empty RelStr for T,T9 being non empty
reflexive antisymmetric RelStr st the RelStr of S = the RelStr of S9 & the
RelStr of T = the RelStr of T9 holds UPS(S,T) = UPS(S9,T9)
proof
let S,S9 be non empty RelStr;
let T,T9 be non empty reflexive antisymmetric RelStr;
assume that
A1: the RelStr of S = the RelStr of S9 and
A2: the RelStr of T = the RelStr of T9;
T |^ the carrier of S = T9 |^ the carrier of S9 by A1,A2,Th15;
then
A3: UPS(S9,T9) is full SubRelStr of T |^ the carrier of S by Def4;
A4: the carrier of UPS(S,T) = the carrier of UPS(S9,T9)
proof
thus the carrier of UPS(S,T) c= the carrier of UPS(S9,T9)
proof
let x be object;
assume x in the carrier of UPS(S,T);
then reconsider x1=x as directed-sups-preserving Function of S,T by Def4;
reconsider y=x1 as Function of S9,T9 by A1,A2;
y is directed-sups-preserving
proof
let X be Subset of S9;
reconsider Y=X as Subset of S by A1;
assume X is non empty directed;
then Y is non empty directed by A1,WAYBEL_0:3;
then x1 preserves_sup_of Y by WAYBEL_0:def 37;
hence thesis by A1,A2,WAYBEL_0:65;
end;
hence thesis by Def4;
end;
let x be object;
assume x in the carrier of UPS(S9,T9);
then reconsider x1=x as directed-sups-preserving Function of S9,T9 by Def4;
reconsider y=x1 as Function of S,T by A1,A2;
y is directed-sups-preserving
proof
let X be Subset of S;
reconsider Y=X as Subset of S9 by A1;
assume X is non empty directed;
then Y is non empty directed by A1,WAYBEL_0:3;
then x1 preserves_sup_of Y by WAYBEL_0:def 37;
hence thesis by A1,A2,WAYBEL_0:65;
end;
hence thesis by Def4;
end;
UPS(S,T) is full SubRelStr of T |^ the carrier of S by Def4;
hence thesis by A3,A4,YELLOW_0:57;
end;
registration
let S, T be complete LATTICE;
cluster UPS(S, T) -> complete;
coherence
proof
set T9 = the Scott TopAugmentation of T;
set S9 = the Scott TopAugmentation of S;
reconsider S9,T9 as complete Scott TopLattice;
A1: the RelStr of T = the RelStr of T9 by YELLOW_9:def 4;
the RelStr of S = the RelStr of S9 by YELLOW_9:def 4;
then UPS(S,T) = UPS(S9,T9) by A1,Th25
.= SCMaps(S9,T9) by Th24
.= ContMaps(S9,T9) by WAYBEL24:38;
hence thesis;
end;
end;
theorem Th26:
for S,T being complete LATTICE holds UPS(S, T) is
sups-inheriting SubRelStr of T|^the carrier of S
proof
let S,T be complete LATTICE;
set S9 = the Scott TopAugmentation of S;
set T9 = the Scott TopAugmentation of T;
A1: the RelStr of T = the RelStr of T9 by YELLOW_9:def 4;
then
A2: T9|^the carrier of S = T|^the carrier of S by Th15;
A3: the RelStr of S = the RelStr of S9 by YELLOW_9:def 4;
then UPS(S,T) = UPS(S9,T9) by A1,Th25
.= SCMaps(S9,T9) by Th24
.= ContMaps(S9,T9) by WAYBEL24:38;
hence thesis by A2,A3,WAYBEL24:35;
end;
theorem Th27:
for S,T being complete LATTICE for A being Subset of UPS(S, T)
holds sup A = "\/"(A, T|^the carrier of S)
proof
let S,T be complete LATTICE;
let A be Subset of UPS(S, T);
A1: UPS(S, T) is sups-inheriting full SubRelStr of T|^the carrier of S by Def4
,Th26;
ex_sup_of A,T|^the carrier of S by YELLOW_0:17;
then "\/"(A,T|^the carrier of S) in the carrier of UPS(S,T) by A1,
YELLOW_0:def 19;
hence thesis by A1,YELLOW_0:68;
end;
definition
let S1,S2,T1,T2 be non empty reflexive antisymmetric RelStr;
let f be Function of S1, S2 such that
A1: f is directed-sups-preserving;
let g be Function of T1, T2 such that
A2: g is directed-sups-preserving;
func UPS(f,g) -> Function of UPS(S2, T1), UPS(S1, T2) means
: Def5:
for h being directed-sups-preserving Function of S2, T1 holds it.h = g*h*f;
existence
proof
defpred P[set,set] means for h being Function st h = $1 holds $2 = g*h*f;
A3: for x being Element of UPS(S2, T1) ex y being Element of UPS(S1, T2)
st P[x,y]
proof
let x be Element of UPS(S2, T1);
reconsider h=x as directed-sups-preserving Function of S2, T1 by Def4;
h*f is directed-sups-preserving Function of S1, T1 by A1,WAYBEL20:28;
then g*(h*f) is directed-sups-preserving Function of S1, T2 by A2,
WAYBEL20:28;
then g*h*f is directed-sups-preserving Function of S1, T2 by RELAT_1:36;
then reconsider y = g*h*f as Element of UPS(S1, T2) by Def4;
take y;
thus thesis;
end;
consider j being Function of the carrier of UPS(S2, T1), the carrier of
UPS(S1, T2) such that
A4: for x being Element of UPS(S2, T1) holds P[x,j.x] from FUNCT_2:sch
3(A3 );
reconsider F=j as Function of UPS(S2, T1), UPS(S1, T2);
take F;
let h be directed-sups-preserving Function of S2, T1;
h is Element of UPS(S2, T1) by Def4;
hence thesis by A4;
end;
uniqueness
proof
let U1,U2 be Function of UPS(S2, T1), UPS(S1, T2);
assume that
A5: for h being directed-sups-preserving Function of S2, T1 holds U1.
h = g*h*f and
A6: for h being directed-sups-preserving Function of S2, T1 holds U2.
h = g*h*f;
for x being object st x in the carrier of UPS(S2, T1) holds U1.x = U2.x
proof
let x be object;
assume x in the carrier of UPS(S2, T1);
then reconsider h=x as directed-sups-preserving Function of S2, T1 by
Def4;
thus U1.x = g*h*f by A5
.= U2.x by A6;
end;
hence U1=U2 by FUNCT_2:12;
end;
end;
:: 2.6. PROPOSITOION, p. 115
:: preservation of composition
theorem Th28:
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
let S1,S2,S3,T1,T2,T3 be non empty Poset;
let f1 be directed-sups-preserving Function of S2, S3;
let f2 be directed-sups-preserving Function of S1, S2;
let g1 be directed-sups-preserving Function of T1, T2;
let g2 be directed-sups-preserving Function of T2, T3;
reconsider F = f1*f2 as directed-sups-preserving Function of S1, S3 by
WAYBEL20:28;
reconsider G = g2*g1 as directed-sups-preserving Function of T1, T3 by
WAYBEL20:28;
for h being directed-sups-preserving Function of S3, T1 holds (UPS(f2,
g2)*UPS(f1, g1)).h = G*h*F
proof
let h be directed-sups-preserving Function of S3, T1;
g1*h is directed-sups-preserving Function of S3,T2 by WAYBEL20:28;
then reconsider
ghf=g1*h*f1 as directed-sups-preserving Function of S2, T2 by WAYBEL20:28;
dom UPS(f1, g1) = the carrier of UPS(S3, T1) by FUNCT_2:def 1;
then h in dom UPS(f1, g1) by Def4;
then (UPS(f2, g2)*UPS(f1, g1)).h = UPS(f2, g2).(UPS(f1, g1).h) by
FUNCT_1:13
.= UPS(f2, g2).(g1*h*f1) by Def5;
hence (UPS(f2, g2)*UPS(f1, g1)).h = g2*(ghf)*f2 by Def5
.= g2*((g1*h*f1)*f2) by RELAT_1:36
.= g2*((g1*(h*f1))*f2) by RELAT_1:36
.= g2*(g1*((h*f1)*f2)) by RELAT_1:36
.= g2*(g1*(h*(f1*f2))) by RELAT_1:36
.= g2*((g1*h)*(f1*f2)) by RELAT_1:36
.= (g2*(g1*h))*(f1*f2) by RELAT_1:36
.= G*h*F by RELAT_1:36;
end;
hence thesis by Def5;
end;
:: 2.6. PROPOSITOION, p. 115
:: preservation of identities
theorem Th29:
for S,T being non empty reflexive antisymmetric RelStr holds UPS
(id S, id T) = id UPS(S, T)
proof
let S,T be non empty reflexive antisymmetric RelStr;
A1: for x being object st x in the carrier of UPS(S, T)
holds UPS(id S, id T).x = x
proof
let x be object;
assume x in the carrier of UPS(S, T);
then reconsider f=x as directed-sups-preserving Function of S, T by Def4;
UPS(id S, id T).f = (id T)*f*(id S) by Def5
.= f*(id S) by FUNCT_2:17;
hence thesis by FUNCT_2:17;
end;
dom UPS(id S, id T) = the carrier of UPS(S, T) by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:17;
end;
:: 2.6. PROPOSITOION, p. 115
:: preservation of directed-sups
theorem Th30:
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
let S1,S2, T1,T2 be complete LATTICE;
let f be directed-sups-preserving Function of S1, S2;
let g be directed-sups-preserving Function of T1, T2;
let A be Subset of UPS(S2, T1);
assume A is non empty directed;
then reconsider H = A as directed non empty Subset of UPS(S2, T1);
assume ex_sup_of A, UPS(S2, T1);
thus ex_sup_of UPS(f, g).:A, UPS(S1, T2) by YELLOW_0:17;
UPS(S2, T1) is full SubRelStr of T1|^the carrier of S2 by Def4;
then reconsider
B = H as directed non empty Subset of T1|^the carrier of S2 by YELLOW_2:7;
A1: UPS(S1, T2) is full SubRelStr of T2|^the carrier of S1 by Def4;
then reconsider
fgsA = UPS(f, g).sup H as Element of T2|^the carrier of S1 by YELLOW_0:58;
the carrier of UPS(S1, T2) c= the carrier of T2|^the carrier of S1 by A1,
YELLOW_0:def 13;
then reconsider
fgA = UPS(f, g).:H as non empty Subset of T2|^the carrier of S1
by XBOOLE_1:1;
A2: T2|^the carrier of S1 = product ((the carrier of S1) --> T2) by
YELLOW_1:def 5;
then
A3: dom sup fgA = the carrier of S1 by WAYBEL_3:27;
A4: T1|^the carrier of S2 = product ((the carrier of S2) --> T1) by
YELLOW_1:def 5;
A5: now
reconsider BB=B as directed Subset of product ((the carrier of S2) --> T1)
by A4;
let s be object;
A6: dom f = the carrier of S1 by FUNCT_2:def 1;
assume s in the carrier of S1;
then reconsider x = s as Element of S1;
reconsider sH = sup H as directed-sups-preserving Function of S2,T1 by Def4
;
A7: ((the carrier of S2) --> T1).(f.x) = T1;
dom sH = the carrier of S2 by FUNCT_2:def 1;
then f.x in dom sH;
then
A8: x in dom (sH*f) by A6,FUNCT_1:11;
A9: pi(fgA, x) = g.:pi(A, f.x)
proof
thus pi(fgA, x) c= g.:pi(A, f.x)
proof
let a be object;
A10: dom g = the carrier of T1 by FUNCT_2:def 1;
assume a in pi(fgA, x);
then consider F being Function such that
A11: F in fgA and
A12: a = F.x by CARD_3:def 6;
consider G being object such that
A13: G in dom UPS(f, g) and
A14: G in H and
A15: F = UPS(f, g).G by A11,FUNCT_1:def 6;
reconsider G as directed-sups-preserving Function of S2, T1 by A13,Def4
;
A16: G.(f.x) in pi(A, f.x) by A14,CARD_3:def 6;
A17: dom f = the carrier of S1 by FUNCT_2:def 1;
dom G = the carrier of S2 by FUNCT_2:def 1;
then f.x in dom G;
then
A18: x in dom (G*f) by A17,FUNCT_1:11;
a = (g*G*f).x by A12,A15,Def5
.= (g*(G*f)).x by RELAT_1:36
.= g.((G*f).x) by A18,FUNCT_1:13
.= g.(G.(f.x)) by A17,FUNCT_1:13;
hence thesis by A10,A16,FUNCT_1:def 6;
end;
let a be object;
A19: dom UPS(f, g) = the carrier of UPS(S2, T1) by FUNCT_2:def 1;
assume a in g.:pi(A, f.x);
then consider F being object such that
F in dom g and
A20: F in pi(A, f.x) and
A21: a = g.F by FUNCT_1:def 6;
consider G being Function such that
A22: G in A and
A23: F = G.(f.x) by A20,CARD_3:def 6;
reconsider G as directed-sups-preserving Function of S2, T1 by A22,Def4;
g*G*f = UPS(f, g).G by Def5;
then
A24: g*G*f in fgA by A22,A19,FUNCT_1:def 6;
A25: dom f = the carrier of S1 by FUNCT_2:def 1;
dom G = the carrier of S2 by FUNCT_2:def 1;
then f.x in dom G;
then
A26: x in dom (G*f) by A25,FUNCT_1:11;
a = g.((G*f).x) by A21,A23,A25,FUNCT_1:13
.= (g*(G*f)).x by A26,FUNCT_1:13
.= (g*G*f).x by RELAT_1:36;
hence thesis by A24,CARD_3:def 6;
end;
A27: ex_sup_of pi(B, f.x), T1 by YELLOW_0:17;
A28: pi(BB, f.x) is directed by YELLOW16:35;
A29: g preserves_sup_of pi(B, f.x) by A28,WAYBEL_0:def 37;
((the carrier of S1) --> T2).x = T2;
hence (sup fgA).s = sup pi(fgA, x) by A2,YELLOW16:33,YELLOW_0:17
.= g.sup pi(B, f.x) by A9,A29,A27
.= g.((sup B).(f.x)) by A4,A7,YELLOW16:33,YELLOW_0:17
.= g.(sH.(f.x)) by Th27
.= g.((sH*f).x) by A6,FUNCT_1:13
.= (g*(sH*f)).x by A8,FUNCT_1:13
.= (g*sH*f).s by RELAT_1:36
.= fgsA.s by Def5;
end;
A30: dom fgsA = the carrier of S1 by A2,WAYBEL_3:27;
thus sup (UPS(f, g).:A) = sup fgA by Th27
.= UPS(f, g).sup A by A3,A30,A5;
end;
theorem Th31:
Omega Sierpinski_Space is Scott
proof
BoolePoset{0} = InclPoset bool {0} by YELLOW_1:4;
then
A1: the carrier of BoolePoset{0} = {0,1} by YELLOW14:1,YELLOW_1:1;
set S = the strict Scott TopAugmentation of BoolePoset{0};
A2: the topology of S = the topology of Sierpinski_Space by WAYBEL18:12;
A3: the RelStr of S = BoolePoset{0} by YELLOW_9:def 4;
the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then Omega Sierpinski_Space = Omega S by A2,A3,A1,WAYBEL25:13
.= S by WAYBEL25:15;
hence thesis;
end;
theorem
for S being complete Scott TopLattice holds oContMaps(S,
Sierpinski_Space) = UPS(S, BoolePoset{0})
proof
reconsider B1 = BoolePoset{0} as complete LATTICE;
reconsider OSS = Omega Sierpinski_Space as Scott complete TopAugmentation of
B1 by Th31,WAYBEL26:4;
let S be complete Scott TopLattice;
A1: the RelStr of S = the RelStr of S;
the TopStruct of OSS = the TopStruct of Sierpinski_Space by WAYBEL25:def 2;
then Omega OSS = OSS by WAYBEL25:13;
then
A2: the RelStr of OSS = the RelStr of B1 by WAYBEL25:16;
thus oContMaps(S, Sierpinski_Space) = ContMaps(S, Omega Sierpinski_Space) by
WAYBEL26:def 1
.= SCMaps(S, OSS) by WAYBEL24:38
.= UPS(S, OSS) by Th24
.= UPS(S,BoolePoset{0}) by A1,A2,Th25;
end;
:: 2.7. LEMMA, p. 116
theorem Th33:
for S being complete LATTICE ex F being Function of UPS(S,
BoolePoset{0}), InclPoset sigma S st F is isomorphic & for f being
directed-sups-preserving Function of S, BoolePoset{0} holds F.f = f"{1}
proof
set T = BoolePoset{0};
reconsider T9 = Omega Sierpinski_Space as Scott TopAugmentation of T by Th31,
WAYBEL26:4;
let S be complete LATTICE;
set S9 = the Scott TopAugmentation of S;
A1: T = the RelStr of T9 by YELLOW_9:def 4;
A2: the topology of S9 = sigma S by YELLOW_9:51;
the RelStr of S = the RelStr of S9 by YELLOW_9:def 4;
then UPS(S, T) = UPS(S9, T9) by A1,Th25
.= SCMaps(S9, T9) by Th24
.= ContMaps(S9, T9) by WAYBEL24:38
.= oContMaps(S9, Sierpinski_Space) by WAYBEL26:def 1;
then consider G being Function of InclPoset sigma S, UPS(S, T) such that
A3: G is isomorphic and
A4: for V being open Subset of S9 holds G.V = chi(V, the carrier of S9)
by A2,WAYBEL26:5;
take F = G";
A5: rng G = [#]UPS(S,T) by A3,WAYBEL_0:66;
then G is onto by FUNCT_2:def 3;
then
A6: F = G qua Function" by A3,TOPS_2:def 4;
hence F is isomorphic by A3,WAYBEL_0:68;
let f be directed-sups-preserving Function of S, T;
f in the carrier of UPS(S, T) by Def4;
then consider V being object such that
A7: V in dom G and
A8: f = G.V by A5,FUNCT_1:def 3;
dom G = the carrier of InclPoset sigma S by FUNCT_2:def 1
.= sigma S by YELLOW_1:1;
then reconsider V as open Subset of S9 by A2,A7,PRE_TOPC:def 2;
thus F.f = V by A3,A6,A7,A8,FUNCT_1:34
.= chi(V, the carrier of S9)"{1} by Th13
.= f"{1} by A4,A8;
end;
theorem Th34:
for S being complete LATTICE holds UPS(S, BoolePoset{0}),
InclPoset sigma S are_isomorphic
proof
let S be complete LATTICE;
consider F being Function of UPS(S, BoolePoset{0}), InclPoset sigma S such
that
A1: F is isomorphic and
for f being directed-sups-preserving Function of S, BoolePoset{0} holds F
.f = f"{1} by Th33;
take F;
thus thesis by A1;
end;
theorem Th35:
for S1, S2, T1, T2 being complete LATTICE for f being Function
of S1, S2, g being Function of T1, T2 st f is isomorphic & g is isomorphic
holds UPS(f, g) is isomorphic
proof
let S1, S2, T1, T2 be complete LATTICE;
let f be Function of S1, S2, g be Function of T1, T2;
assume that
A1: f is isomorphic and
A2: g is isomorphic;
A3: g is sups-preserving Function of T1, T2 by A2,WAYBEL13:20;
A4: f is sups-preserving Function of S1, S2 by A1,WAYBEL13:20;
then
A5: UPS(f,g) is directed-sups-preserving Function of UPS(S2, T1), UPS(S1, T2
) by A3,Th30;
consider g9 being monotone Function of T2,T1 such that
A6: g*g9 = id T2 and
A7: g9*g = id T1 by A2,YELLOW16:15;
g9 is isomorphic by A2,A6,A7,YELLOW16:15;
then
A8: g9 is sups-preserving Function of T2, T1 by WAYBEL13:20;
consider f9 being monotone Function of S2,S1 such that
A9: f*f9 = id S2 and
A10: f9*f = id S1 by A1,YELLOW16:15;
f9 is isomorphic by A1,A9,A10,YELLOW16:15;
then
A11: f9 is sups-preserving Function of S2, S1 by WAYBEL13:20;
then
A12: UPS(f9,g9) is directed-sups-preserving Function of UPS(S1, T2), UPS( S2
, T1 ) by A8,Th30;
A13: UPS(f9,g9)*UPS(f,g) = UPS(id S2, id T1) by A4,A3,A9,A7,A11,A8,Th28
.= id UPS(S2,T1) by Th29;
UPS(f,g)*UPS(f9,g9) = UPS(id S1, id T2) by A4,A3,A10,A6,A11,A8,Th28
.= id UPS(S1,T2) by Th29;
hence thesis by A13,A5,A12,YELLOW16:15;
end;
theorem Th36:
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
let S1, S2, T1, T2 be complete LATTICE;
given f being Function of S1, S2 such that
A1: f is isomorphic;
given g being Function of T1, T2 such that
A2: g is isomorphic;
take UPS(f, g);
thus thesis by A1,A2,Th35;
end;
theorem Th37:
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
let S,T be complete LATTICE;
let f be directed-sups-preserving projection Function of T,T;
reconsider If = Image f as complete LATTICE by YELLOW_2:35;
A1: (If)|^ the carrier of S is full SubRelStr of T |^ the carrier of S by
YELLOW16:39;
UPS(S, If) is full SubRelStr of (Image f)|^ the carrier of S by Def4;
then reconsider
UPSIf=UPS(S, If) as full SubRelStr of T |^ the carrier of S by A1,WAYBEL15:1;
UPS(S, T) is full SubRelStr of T |^ the carrier of S by Def4;
then reconsider
IUPS=Image UPS(id S,f) as full SubRelStr of T|^the carrier of S
by WAYBEL15:1;
the carrier of UPSIf = the carrier of IUPS
proof
thus the carrier of UPSIf c= the carrier of IUPS
proof
let x be object;
A2: dom UPS(id S, f) = the carrier of UPS(S, T) by FUNCT_2:def 1;
assume x in the carrier of UPSIf;
then reconsider h=x as directed-sups-preserving Function of S, If by Def4
;
the carrier of If c= the carrier of T by YELLOW_0:def 13;
then
A3: rng h c= the carrier of T;
dom h = the carrier of S by FUNCT_2:def 1;
then reconsider g=h as Function of S, T by A3,RELSET_1:4;
A4: g is directed-sups-preserving
proof
let X be Subset of S;
assume
A5: X is non empty directed;
thus g preserves_sup_of X
proof
reconsider hX = h.:X as non empty directed Subset of If by A5,
YELLOW_2:15;
assume
A6: ex_sup_of X,S;
h preserves_sup_of X by A5,WAYBEL_0:def 37;
then
A7: sup (hX) = h.sup X by A6;
thus
A8: ex_sup_of g.:X,T by YELLOW_0:17;
If is directed-sups-inheriting non empty full SubRelStr of T by
YELLOW_2:35;
hence thesis by A7,A8,WAYBEL_0:7;
end;
end;
then
A9: g in the carrier of UPS(S, T) by Def4;
UPS(id S, f).g = f*g*(id S) by A4,Def5
.= h*(id S) by Th10
.= g by FUNCT_2:17;
then x in rng UPS(id S, f) by A9,A2,FUNCT_1:def 3;
hence thesis by YELLOW_0:def 15;
end;
let x be object;
A10: rng f = the carrier of subrelstr rng f by YELLOW_0:def 15;
assume x in the carrier of IUPS;
then x in rng UPS(id S, f) by YELLOW_0:def 15;
then consider a being object such that
A11: a in dom UPS(id S, f) and
A12: x = UPS(id S, f).a by FUNCT_1:def 3;
reconsider a as directed-sups-preserving Function of S, T by A11,Def4;
A13: x = f*a*(id S) by A12,Def5
.= f*a by FUNCT_2:17;
then reconsider x0=x as directed-sups-preserving Function of S,T by
WAYBEL15:11;
A14: rng x0 c= the carrier of T;
dom x0 = the carrier of S by FUNCT_2:def 1;
then reconsider x1 = x0 as Function of S, If by A10,A13,A14,FUNCT_2:2
,RELAT_1:26;
x1 is directed-sups-preserving
proof
let X be Subset of S;
assume
A15: X is non empty directed;
thus x1 preserves_sup_of X
proof
reconsider hX = x0.:X as non empty directed Subset of T by A15,
YELLOW_2:15;
A16: If is directed-sups-inheriting non empty full SubRelStr of T by
YELLOW_2:35;
reconsider gX = x1.:X as non empty directed Subset of If by Th12,A15,
YELLOW_2:15;
assume
A17: ex_sup_of X,S;
thus ex_sup_of x1.:X,If by YELLOW_0:17;
A18: x0 preserves_sup_of X by A15,WAYBEL_0:def 37;
then ex_sup_of x0.:X,T by A17;
then sup (gX) = sup (hX) by A16,WAYBEL_0:7;
hence thesis by A17,A18;
end;
end;
hence thesis by Def4;
end;
hence thesis by YELLOW_0:57;
end;
Lm1: now
let M be non empty set, X,Y be non empty Poset;
let f be directed-sups-preserving Function of X, Y|^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;
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 & 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;
end;
theorem Th38:
for X being non empty set, 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
let M be non empty set, X,Y be non empty Poset;
let f be directed-sups-preserving Function of X, Y|^M;
let i be Element of M;
A1: (M --> Y).i = Y;
dom commute f = M by Lm1;
then
A2: (commute f).i in rng commute f by FUNCT_1:def 3;
A3: f in Funcs(the carrier of X, Funcs(M, the carrier of Y)) by Lm1;
then f is Function of the carrier of X, Funcs(M, the carrier of Y) by
FUNCT_2:66;
then
A4: rng f c= Funcs(M, the carrier of Y) by RELAT_1:def 19;
rng commute f c= Funcs(the carrier of X, the carrier of Y) by Lm1;
then consider g being Function such that
A5: (commute f).i = g and
A6: dom g = the carrier of X and
A7: rng g c= the carrier of Y by A2,FUNCT_2:def 2;
reconsider g as Function of X,Y by A6,A7,FUNCT_2:2;
A8: Y|^M = product (M --> Y) by YELLOW_1:def 5;
g is directed-sups-preserving
proof
let A be Subset of X;
assume A is non empty directed;
then reconsider B = A as non empty directed Subset of X;
assume
A9: ex_sup_of A, X;
A10: f preserves_sup_of B by WAYBEL_0:def 37;
then
A11: ex_sup_of f.:B, Y|^M by A9;
then ex_sup_of pi(f.:A, i), Y by A8,A1,YELLOW16:31;
hence ex_sup_of g.:A, Y by A4,A5,Th8;
A12: pi(f.:A, i) = g.:A by A4,A5,Th8;
sup (f.:B) = f.sup B by A9,A10;
then sup pi(f.:A, i) = (f.sup A).i by A11,A8,A1,YELLOW16:33;
hence thesis by A3,A5,A12,FUNCT_6:56;
end;
hence thesis by A5;
end;
theorem Th39:
for X being non empty set, 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
let M be non empty set, X,Y be non empty Poset;
let f be directed-sups-preserving Function of X, Y|^M;
A1: rng commute f c= the carrier of UPS(X, Y)
proof
let g be object;
assume g in rng commute f;
then consider i being object such that
A2: i in dom commute f and
A3: g = (commute f).i by FUNCT_1:def 3;
reconsider i as Element of M by A2,Lm1;
(commute f).i is directed-sups-preserving Function of X, Y by Th38;
hence thesis by A3,Def4;
end;
dom commute f = M by Lm1;
hence thesis by A1,FUNCT_2:2;
end;
theorem Th40:
for X being non empty set, 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
let X be non empty set, S,T be non empty Poset;
let f be Function of X, the carrier of UPS(S, T);
A1: the carrier of T|^X = Funcs(X, the carrier of T) by YELLOW_1:28;
A2: f in Funcs(X, the carrier of UPS(S, T)) by FUNCT_2:8;
A3: Funcs(X, the carrier of UPS(S, T)) c= Funcs(X, Funcs(the carrier of S,
the carrier of T)) by Th22,FUNCT_5:56;
then
commute f in Funcs(the carrier of S, Funcs(X, the carrier of T)) by A2,
FUNCT_6:55;
then reconsider g = commute f as Function of S, T|^X by A1,FUNCT_2:66;
A4: rng g c= Funcs(X, the carrier of T) by A1;
g is directed-sups-preserving
proof
let A be Subset of S;
assume A is non empty directed;
then reconsider B = A as directed non empty Subset of S;
A5: T|^X = product (X --> T) by YELLOW_1:def 5;
then
A6: dom (g.sup A) = X by WAYBEL_3:27;
assume
A7: ex_sup_of A, S;
now
let x be Element of X;
reconsider fx = f.x as directed-sups-preserving Function of S, T by Def4;
A8: fx preserves_sup_of B by WAYBEL_0:def 37;
commute g = f by A3,A2,FUNCT_6:57;
then
A9: fx.:A = pi(g.:A, x) by A4,Th8;
thus ex_sup_of pi(g.:A, x), (X --> T).x by A9,A8,A7;
end;
hence
A10: ex_sup_of g.:A, T|^X by A5,YELLOW16:31;
A11: now
let x be object;
assume x in X;
then reconsider a = x as Element of X;
reconsider fx = f.a as directed-sups-preserving Function of S, T by Def4;
A12: (X --> T).a = T;
commute g = f by A3,A2,FUNCT_6:57;
then
A13: fx.:A = pi(g.:A, a) by A4,Th8;
fx preserves_sup_of B by WAYBEL_0:def 37;
then sup pi(g.:B, a) = fx.sup A by A13,A7;
then fx.sup A = (sup (g.:B)).a by A5,A10,A12,YELLOW16:33;
hence (sup (g.:A)).x = (g.sup A).x by A3,A2,FUNCT_6:56;
end;
dom sup (g.:A) = X by A5,WAYBEL_3:27;
hence thesis by A11,A6;
end;
hence thesis;
end;
theorem Th41:
for X being non empty set, S,T being non empty Poset ex F being
Function of UPS(S, T|^X), UPS(S, T)|^X st F is commuting isomorphic
proof
deffunc F(Function) = commute $1;
let X be non empty set, S, T be non empty Poset;
consider F being ManySortedSet of the carrier of UPS(S, T|^X) such that
A1: for f being Element of UPS(S, T|^X) holds F.f = F(f) from PBOOLE:sch
5;
A2: dom F = the carrier of UPS(S, T|^X) by PARTFUN1:def 2;
A3: rng F c= the carrier of UPS(S, T)|^X
proof
let g be object;
assume g in rng F;
then consider f being object such that
A4: f in dom F and
A5: g = F.f by FUNCT_1:def 3;
reconsider f as directed-sups-preserving Function of S, T|^X by A4,Def4;
g = commute f by A1,A4,A5;
then reconsider g as Function of X, the carrier of UPS(S, T) by Th39;
A6: rng g c= the carrier of UPS(S, T);
dom g = X by FUNCT_2:def 1;
then g in Funcs(X, the carrier of UPS(S, T)) by A6,FUNCT_2:def 2;
hence thesis by YELLOW_1:28;
end;
then reconsider F as Function of UPS(S, T|^X), UPS(S, T)|^X by A2,FUNCT_2:2;
take F;
consider G being ManySortedSet of the carrier of UPS(S, T)|^X such that
A7: for f being Element of UPS(S, T)|^X holds G.f = F(f) from PBOOLE:
sch 5;
A8: dom G = the carrier of UPS(S, T)|^X by PARTFUN1:def 2;
A9: rng G c= the carrier of UPS(S, T|^X)
proof
let g be object;
assume g in rng G;
then consider f being object such that
A10: f in dom G and
A11: g = G.f by FUNCT_1:def 3;
the carrier of UPS(S, T)|^X = Funcs(X, the carrier of UPS(S, T)) by
YELLOW_1:28;
then reconsider f as Function of X, the carrier of UPS(S, T) by A10,
FUNCT_2:66;
g = commute f by A7,A10,A11;
then g is directed-sups-preserving Function of S, T|^X by Th40;
hence thesis by Def4;
end;
then reconsider G as Function of UPS(S, T)|^X, UPS(S, T|^X) by A8,FUNCT_2:2;
A12: G is commuting
proof
hereby
let x be set;
assume x in dom G;
then x in Funcs(X, the carrier of UPS(S, T)) by A8,YELLOW_1:28;
then x is Function of X, the carrier of UPS(S, T) by FUNCT_2:66;
hence x is Function-yielding Function;
end;
thus thesis by A7,A8;
end;
A13: the carrier of T|^X = Funcs(X, the carrier of T) by YELLOW_1:28;
UPS(S, T) is full SubRelStr of T|^the carrier of S by Def4;
then
A14: UPS(S, T)|^X is full SubRelStr of (T|^the carrier of S)|^X by YELLOW16:39;
A15: UPS(S, T|^X) is full SubRelStr of (T|^X)|^the carrier of S by Def4;
then
A16: G is monotone by A12,A14,Th19;
thus
A17: F is commuting
proof
hereby
let x be set;
assume x in dom F;
then x is Function of S, T|^X by Def4;
hence x is Function-yielding Function;
end;
thus thesis by A1,A2;
end;
then
A18: F is monotone by A15,A14,Th19;
the carrier of UPS(S, T)|^X = Funcs(X, the carrier of UPS(S, T)) by
YELLOW_1:28;
then the carrier of UPS(S, T)|^X c= Funcs(X, Funcs(the carrier of S, the
carrier of T)) by Th22,FUNCT_5:56;
then
A19: F*G = id (UPS(S, T)|^X) by A2,A8,A9,A17,A12,Th3;
the carrier of UPS(S, T|^X) c= Funcs(the carrier of S, the carrier of T
|^X) by Th22;
then G*F = id UPS(S, T|^X) by A2,A3,A8,A17,A12,A13,Th3;
hence thesis by A19,A18,A16,YELLOW16:15;
end;
theorem Th42:
for X being non empty set, S,T being non empty Poset holds UPS(S
, T|^X), UPS(S, T)|^X are_isomorphic
proof
let X be non empty set, S, T be non empty Poset;
consider F being Function of UPS(S, T|^X), UPS(S, T)|^X such that
A1: F is commuting isomorphic by Th41;
take F;
thus thesis by A1;
end;
:: 2.8. THEOREM, p. 116
:: [CONT -> CONT] is into CONT (so [CONT -> CONT] is functor)
theorem
for S,T being continuous complete LATTICE holds UPS(S,T) is continuous
proof
let S, T be continuous complete LATTICE;
consider X being non empty set, p being projection Function of BoolePoset X,
BoolePoset X such that
A1: p is directed-sups-preserving and
A2: T, Image p are_isomorphic by WAYBEL15:18;
A3: (id S)*id S = id S by QUANTAL1:def 9;
Image p is complete non empty Poset by A2,WAYBEL20:18;
then UPS(S, T), UPS(S, Image p) are_isomorphic by A2,Th36;
then
A4: UPS(S, T), Image UPS(id S, p) are_isomorphic by A1,Th37;
set L = the Scott TopAugmentation of S;
A5: InclPoset sigma L is continuous by WAYBEL14:36;
A6: UPS(S, BoolePoset{0}), InclPoset sigma S are_isomorphic by Th34;
p*p = p by QUANTAL1:def 9;
then UPS(id S, p) * UPS(id S, p) = UPS(id S, p) by A3,A1,Th28;
then UPS(id S, p) is directed-sups-preserving idempotent Function of UPS(S,
BoolePoset X), UPS(S, BoolePoset X) by A1,Th30,QUANTAL1:def 9;
then
A7: UPS(id S, p) is directed-sups-preserving projection Function of UPS(S,
BoolePoset X), UPS(S, BoolePoset X) by WAYBEL_1:def 13;
BoolePoset X, (BoolePoset{0})|^X are_isomorphic by Th18;
then
A8: UPS(S, BoolePoset X), UPS(S, (BoolePoset{0})|^X) are_isomorphic by Th36;
the RelStr of L = the RelStr of S by YELLOW_9:def 4;
then InclPoset sigma S is continuous by A5,YELLOW_9:52;
then UPS(S, BoolePoset{0}) is continuous complete
by A6,WAYBEL15:9,WAYBEL_1:6;
then for x being Element of X holds (X --> UPS(S, BoolePoset{0})).x is
continuous complete LATTICE;
then X-POS_prod(X --> UPS(S, BoolePoset{0})) is continuous by WAYBEL20:33;
then
A9: UPS(S, BoolePoset{0})|^X is continuous by YELLOW_1:def 5;
UPS(S, (BoolePoset{0})|^X), UPS(S, BoolePoset{0})|^X are_isomorphic by Th42;
then UPS(S, BoolePoset X), UPS(S, BoolePoset{0})|^X are_isomorphic by A8,
WAYBEL_1:7;
then UPS(S, BoolePoset X) is continuous LATTICE by A9,WAYBEL15:9,WAYBEL_1:6;
then Image UPS(id S, p) is continuous by A7,WAYBEL15:15;
hence thesis by A4,WAYBEL15:9,WAYBEL_1:6;
end;
:: 2.8. THEOREM, p. 116
:: [ALG -> ALG] is into ALG (so [ALG -> ALG] is functor)
theorem
for S,T being algebraic complete LATTICE holds UPS(S,T) is algebraic
proof
let S, T be algebraic complete LATTICE;
consider X being non empty set, p being closure Function of BoolePoset X,
BoolePoset X such that
A1: p is directed-sups-preserving and
A2: T, Image p are_isomorphic by WAYBEL13:35;
now
let i be Element of UPS(S, BoolePoset X);
reconsider f = i as directed-sups-preserving Function of S, BoolePoset X
by Def4;
A3: UPS(id S, p).f = p*f*(id the carrier of S) by A1,Def5
.= p*f by FUNCT_2:17;
A4: now
let s be Element of S;
A5: id BoolePoset X <= p by WAYBEL_1:def 14;
A6: (id BoolePoset X).(i.s) = i.s;
(p*f).s = p.(f.s) by FUNCT_2:15;
hence i.s <= UPS(id S, p).i.s by A5,A6,A3,YELLOW_2:9;
end;
thus (id UPS(S, BoolePoset X)).i <= UPS(id S, p).i by A4,Th23;
end;
then
A7: (id UPS(S, BoolePoset X)) <= UPS(id S, p) by YELLOW_2:9;
A8: (id S)*id S = id S by QUANTAL1:def 9;
p*p = p by QUANTAL1:def 9;
then UPS(id S, p) * UPS(id S, p) = UPS(id S, p) by A8,A1,Th28;
then UPS(id S, p) is directed-sups-preserving idempotent Function of UPS(S,
BoolePoset X), UPS(S, BoolePoset X) by A1,Th30,QUANTAL1:def 9;
then UPS(id S, p) is projection;
then reconsider
Sp = UPS(id S, p) as directed-sups-preserving closure Function of
UPS(S, BoolePoset X), UPS(S, BoolePoset X) by A7,A1,Th30,WAYBEL_1:def 14;
Image p is complete non empty Poset by A2,WAYBEL20:18;
then UPS(S, T), UPS(S, Image p) are_isomorphic by A2,Th36;
then
A9: UPS(S, T), Image Sp are_isomorphic by A1,Th37;
BoolePoset X, (BoolePoset{0})|^X are_isomorphic by Th18;
then
A10: UPS(S, BoolePoset X), UPS(S, (BoolePoset{0})|^X) are_isomorphic by Th36;
set L = the Scott TopAugmentation of S;
A11: InclPoset sigma S = InclPoset the topology of L by YELLOW_9:51;
A12: the RelStr of L = the RelStr of S by YELLOW_9:def 4;
then L is algebraic by WAYBEL13:26,32;
then ex B being Basis of L st B = {uparrow x where x is Element of L: x in
the carrier of CompactSublatt L} by WAYBEL14:42;
then InclPoset sigma L is algebraic by WAYBEL14:43;
then
A13: InclPoset sigma S is algebraic by A12,YELLOW_9:52;
UPS(S, BoolePoset{0}), InclPoset sigma S are_isomorphic by Th34;
then UPS(S, BoolePoset{0}) is algebraic lower-bounded by A13,A11,WAYBEL13:32
,WAYBEL_1:6;
then X-POS_prod(X --> UPS(S, BoolePoset{0})) is lower-bounded algebraic;
then
A14: UPS(S, BoolePoset{0})|^X is algebraic lower-bounded by YELLOW_1:def 5;
UPS(S, (BoolePoset{0})|^X), UPS(S, BoolePoset{0})|^X are_isomorphic by Th42;
then UPS(S, BoolePoset X), UPS(S, BoolePoset{0})|^X are_isomorphic by A10,
WAYBEL_1:7;
then UPS(S, BoolePoset X) is algebraic lower-bounded LATTICE by A14,
WAYBEL13:32,WAYBEL_1:6;
then
A15: Image Sp is algebraic by WAYBEL_8:24;
Image Sp is complete LATTICE by YELLOW_2:30;
hence thesis by A9,A15,WAYBEL13:32,WAYBEL_1:6;
end;
theorem Th45:
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
let R,S,T be complete LATTICE;
let f be directed-sups-preserving Function of R, UPS(S, T);
A1: f in Funcs(the carrier of R, the carrier of UPS(S, T)) by FUNCT_2:8;
Funcs(the carrier of R, the carrier of UPS(S, T)) c= Funcs(the carrier
of R, Funcs(the carrier of S, the carrier of T)) by Th22,FUNCT_5:56;
then uncurry f in Funcs([:the carrier of R, the carrier of S:], the carrier
of T) by A1,FUNCT_6:11;
then uncurry f in Funcs(the carrier of [:R, S:], the carrier of T) by
YELLOW_3:def 2;
then reconsider g = uncurry f as Function of [:R, S:], T by FUNCT_2:66;
A2: the carrier of UPS(S, T) c= Funcs(the carrier of S, the carrier of T) by
Th22;
now
reconsider ST = UPS(S, T) as full sups-inheriting non empty SubRelStr of T
|^the carrier of S by Def4,Th26;
let a be Element of R, b be Element of S;
reconsider f9 = f as directed-sups-preserving Function of R, ST;
incl(ST, T|^the carrier of S) is directed-sups-preserving by WAYBEL21:10;
then
A3: incl(ST, T|^the carrier of S)*f9 is directed-sups-preserving by WAYBEL20:28
;
the carrier of ST c= the carrier of T|^the carrier of S by YELLOW_0:def 13;
then incl(ST, T|^the carrier of S) = id the carrier of ST by YELLOW_9:def 1
;
then f is directed-sups-preserving Function of R, T|^the carrier of S by A3
,FUNCT_2:17;
then
A4: (commute f).b is directed-sups-preserving Function of R, T by Th38;
rng f c= Funcs(the carrier of S, the carrier of T) by A2;
then curry g = f by FUNCT_5:48;
then Proj(g,a) = f.a by WAYBEL24:def 1;
hence Proj (g, a) is directed-sups-preserving by Def4;
Proj (g, b) = (curry' g).b by WAYBEL24:def 2;
hence Proj (g, b) is directed-sups-preserving by A4,FUNCT_6:def 10;
end;
hence thesis by WAYBEL24:18;
end;
theorem Th46:
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
let R,S,T be complete LATTICE;
A1: [:the carrier of R, the carrier of S:] = the carrier of [:R,S:] by
YELLOW_3:def 2;
let f be directed-sups-preserving Function of [:R,S:], T;
A2: the carrier of UPS([:R,S:], T) c= Funcs(the carrier of [:R,S:], the
carrier of T) by Th22;
f in the carrier of UPS([:R,S:], T) by Def4;
then curry f in Funcs(the carrier of R, Funcs(the carrier of S, the carrier
of T)) by A2,A1,FUNCT_6:10;
then
A3: curry f is Function of the carrier of R, Funcs(the carrier of S, the
carrier of T) by FUNCT_2:66;
then
A4: dom curry f = the carrier of R by FUNCT_2:def 1;
rng curry f c= the carrier of UPS(S, T)
proof
let y be object;
assume y in rng curry f;
then consider x being object such that
A5: x in dom curry f and
A6: y = (curry f).x by FUNCT_1:def 3;
reconsider x as Element of R by A3,A5,FUNCT_2:def 1;
Proj(f, x) is directed-sups-preserving by WAYBEL24:16;
then y is directed-sups-preserving Function of S, T by A6,WAYBEL24:def 1;
hence thesis by Def4;
end;
then reconsider g = curry f as Function of R, UPS(S, T) by A4,FUNCT_2:2;
A7: UPS(S, T) is full SubRelStr of T|^the carrier of S by Def4;
A8: dom f = the carrier of [:R,S:] by FUNCT_2:def 1;
g is directed-sups-preserving
proof
let A be Subset of R;
assume A is non empty directed;
then reconsider B = A as directed non empty Subset of R;
reconsider gsA = g.sup A as Element of T|^the carrier of S by A7,
YELLOW_0:58;
assume ex_sup_of A, R;
thus ex_sup_of g.:A, UPS(S, T) by YELLOW_0:17;
A9: for s be Element of S holds ((the carrier of S) --> T).s is complete
LATTICE;
the carrier of UPS(S, T) c= the carrier of T|^the carrier of S by A7,
YELLOW_0:def 13;
then g.:B c= the carrier of T|^the carrier of S;
then reconsider gA = g.:A as non empty Subset of T|^the carrier of S;
A10: T|^the carrier of S = product ((the carrier of S) --> T) by YELLOW_1:def 5
;
then
A11: dom gsA = the carrier of S by WAYBEL_3:27;
A12: dom gsA = the carrier of S by A10,WAYBEL_3:27;
A13: now
let x be object;
assume x in the carrier of S;
then reconsider s = x as Element of S;
reconsider s1 = {s} as directed non empty Subset of S by WAYBEL_0:5;
reconsider As = [:B,s1:] as non empty directed Subset of [:R,S:];
A14: f preserves_sup_of As by WAYBEL_0:def 37;
A15: ex_sup_of As, [:R,S:] by YELLOW_0:17;
((the carrier of S) --> T).s = T;
hence (sup gA).x = sup pi(gA, s) by A9,A10,WAYBEL_3:32
.= sup (f.:As) by A8,Th9
.= f.sup As by A14,A15
.= f. [sup proj1 As, sup proj2 As] by YELLOW_3:46
.= f. [sup A, sup proj2 As] by FUNCT_5:9
.= f. [sup A, sup {s}] by FUNCT_5:9
.= f.(sup A, s) by YELLOW_0:39
.= gsA.x by A4,A12,FUNCT_5:31;
end;
dom sup gA = the carrier of S by A10,WAYBEL_3:27;
then sup gA = gsA by A13,A11;
hence thesis by Th27;
end;
hence thesis;
end;
:: 2.10. THEOREM, p. 117
theorem
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 isomorphic
proof
deffunc F(Function) = uncurry $1;
let R,S,T be complete LATTICE;
consider F being ManySortedSet of the carrier of UPS(R, UPS(S, T)) such that
A1: for f being Element of UPS(R, UPS(S, T)) holds F.f = F(f) from
PBOOLE:sch 5;
A2: dom F = the carrier of UPS(R, UPS(S, T)) by PARTFUN1:def 2;
A3: rng F c= the carrier of UPS([:R,S:], T)
proof
let g be object;
assume g in rng F;
then consider f being object such that
A4: f in dom F and
A5: g = F.f by FUNCT_1:def 3;
reconsider f as directed-sups-preserving Function of R, UPS(S, T) by A4
,Def4;
g = uncurry f by A1,A4,A5;
then g is directed-sups-preserving Function of [:R, S:], T by Th45;
hence thesis by Def4;
end;
then reconsider F as Function of UPS(R, UPS(S, T)), UPS([:R,S:], T) by A2,
FUNCT_2:2;
take F;
thus
A6: F is uncurrying
proof
hereby
let x be set;
assume x in dom F;
then x is Function of R, UPS(S, T) by Def4;
hence x is Function-yielding Function;
end;
thus thesis by A1,A2;
end;
deffunc F(Function) = curry $1;
consider G being ManySortedSet of the carrier of UPS([:R,S:], T) such that
A7: for f being Element of UPS([:R,S:], T) holds G.f = F(f) from PBOOLE
:sch 5;
A8: dom G = the carrier of UPS([:R,S:], T) by PARTFUN1:def 2;
A9: rng G c= the carrier of UPS(R, UPS(S, T))
proof
let g be object;
assume g in rng G;
then consider f being object such that
A10: f in dom G and
A11: g = G.f by FUNCT_1:def 3;
reconsider f as directed-sups-preserving Function of [:R,S:], T by A10,Def4
;
g = curry f by A7,A10,A11;
then g is directed-sups-preserving Function of R, UPS(S,T) by Th46;
hence thesis by Def4;
end;
then reconsider G as Function of UPS([:R,S:], T), UPS(R, UPS(S, T)) by A8,
FUNCT_2:2;
UPS(S, T) is full SubRelStr of T|^the carrier of S by Def4;
then
A12: UPS(S, T)|^the carrier of R is full SubRelStr of (T|^the carrier of S)
|^the carrier of R by YELLOW16:39;
UPS(R, UPS(S, T)) is full SubRelStr of UPS(S, T)|^the carrier of R by Def4;
then
A13: UPS(R, UPS(S, T)) is full non empty SubRelStr of (T|^the carrier of S)
|^the carrier of R by A12,YELLOW16:26;
the carrier of [:R,S:] = [:the carrier of R, the carrier of S:] by
YELLOW_3:def 2;
then
A14: UPS([:R,S:], T) is full non empty SubRelStr of T|^[:the carrier of R,
the carrier of S:] by Def4;
then
A15: F is monotone by A6,A13,Th20;
A16: G is currying
proof
hereby
let x be set;
assume x in dom G;
then reconsider f = x as Function of [:R, S:], T by Def4;
proj1 f = the carrier of [:R, S:] by FUNCT_2:def 1
.= [:the carrier of R, the carrier of S:] by YELLOW_3:def 2;
hence x is Function & proj1 x is Relation;
end;
thus thesis by A7,A8;
end;
then
A17: G is monotone by A13,A14,Th21;
the carrier of (T|^the carrier of S)|^the carrier of R = Funcs(the
carrier of R, the carrier of T|^the carrier of S) by YELLOW_1:28
.= Funcs(the carrier of R, Funcs(the carrier of S, the carrier of T)) by
YELLOW_1:28;
then the carrier of UPS(R, UPS(S, T)) c= Funcs(the carrier of R, Funcs(the
carrier of S, the carrier of T)) by A13,YELLOW_0:def 13;
then
A18: G*F = id UPS(R, UPS(S, T)) by A2,A3,A8,A6,A16,Th4;
the carrier of T|^[:the carrier of R, the carrier of S:] = Funcs([:the
carrier of R, the carrier of S:], the carrier of T) by YELLOW_1:28;
then
the carrier of UPS([:R,S:], T) c= Funcs([:the carrier of R, the carrier
of S:], the carrier of T) by A14,YELLOW_0:def 13;
then F*G = id UPS([:R,S:], T) by A2,A8,A9,A6,A16,Th5;
hence thesis by A18,A15,A17,YELLOW16:15;
end;