:: Scott-Continuous Functions, Part II
:: by Adam Grabowski
::
:: Received June 22, 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 WAYBEL_0, WAYBEL11, WAYBEL_9, SUBSET_1, WAYBEL17, EQREL_1,
ORDINAL2, FUNCT_1, STRUCT_0, TARSKI, YELLOW_1, XBOOLE_0, ORDERS_2,
RELAT_2, SEQM_3, XXREAL_0, RELAT_1, FUNCOP_1, LATTICES, LATTICE3, NEWTON,
REWRITE1, YELLOW_0, FUNCT_2, ZFMISC_1, BORSUK_1, FUNCT_5, MCART_1,
PRE_TOPC, CAT_1, MONOID_0, WAYBEL_3, PBOOLE, CARD_3, FUNCT_4, WAYBEL24;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_5, MONOID_0, CARD_3, PBOOLE, FUNCOP_1,
STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, FUNCT_7, YELLOW_0, ORDERS_3,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL17,
YELLOW_3;
constructors FUNCT_7, BORSUK_1, MONOID_0, ORDERS_3, WAYBEL_1, WAYBEL_3,
WAYBEL17, YELLOW_3, FUNCT_5;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3,
YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, WAYBEL10,
WAYBEL11, WAYBEL17, PRE_TOPC;
requirements SUBSET, BOOLE;
definitions TARSKI, WAYBEL_0, LATTICE3, ORDERS_2, MONOID_0, XBOOLE_0;
equalities WAYBEL_0, BINOP_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, LATTICE3, ORDERS_2, MONOID_0, XBOOLE_0;
theorems WAYBEL_0, TARSKI, FUNCT_1, FUNCT_2, YELLOW_0, YELLOW_2, WAYBEL_1,
ZFMISC_1, WAYBEL10, WAYBEL17, YELLOW_3, MCART_1, FUNCT_5, YELLOW_5,
YELLOW10, FUNCOP_1, YELLOW_1, WAYBEL_3, CARD_3, FUNCT_7, RELAT_1,
WAYBEL15, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0;
begin :: Preliminaries
theorem
for S, T being up-complete Scott TopLattice for M being Subset of
SCMaps (S,T) holds "\/" (M, SCMaps (S,T)) is continuous Function of S, T
proof
let S, T be up-complete Scott TopLattice;
let M be Subset of SCMaps (S,T);
the carrier of SCMaps (S,T) c= the carrier of MonMaps (S,T) by
YELLOW_0:def 13;
then "\/" (M, SCMaps (S,T)) in the carrier of MonMaps (S,T);
hence thesis by WAYBEL10:9,WAYBEL17:def 2;
end;
registration
let S be non empty RelStr, T be non empty reflexive RelStr;
cluster constant -> monotone for Function of S, T;
coherence
proof
let f be Function of S, T;
assume
A1: f is constant;
for x,y being Element of S st x <= y holds f.x <= f.y
proof
let x,y be Element of S;
assume x <= y;
y in the carrier of S;
then
A2: y in dom f by FUNCT_2:def 1;
x in the carrier of S;
then x in dom f by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:def 10;
end;
hence thesis by WAYBEL_1:def 2;
end;
end;
registration
let S be non empty RelStr, T be reflexive non empty RelStr, a be Element of
T;
cluster S --> a -> monotone;
coherence
proof
set f = S --> a;
for x, y being Element of S st x <= y holds f.x <= f.y
proof
let x, y be Element of S;
assume x <= y;
f.x = ((the carrier of S) --> a). x .= a by FUNCOP_1:7
.= ((the carrier of S) --> a). y by FUNCOP_1:7
.= f.y;
hence thesis;
end;
hence thesis by WAYBEL_1:def 2;
end;
end;
theorem
for S being non empty RelStr, T being lower-bounded antisymmetric
reflexive non empty RelStr holds Bottom MonMaps(S, T) = S --> Bottom T
proof
let S be non empty RelStr, T be lower-bounded antisymmetric reflexive non
empty RelStr;
set L = MonMaps(S, T);
reconsider f = S --> Bottom T as Element of L by WAYBEL10:9;
reconsider f9 = f as Function of S, T;
A1: for b being Element of L st b is_>=_than {} holds f <= b
proof
let b be Element of L;
assume b is_>=_than {};
reconsider b9 = b as Function of S, T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of T|^ the carrier of S by
YELLOW_0:58;
for x being Element of S holds f9.x <= b9.x
proof
let x be Element of S;
f9. x = ((the carrier of S) --> Bottom T). x .= Bottom T by FUNCOP_1:7;
hence thesis by YELLOW_0:44;
end;
then f9 <= b9 by YELLOW_2:9;
then f99 <= b99 by WAYBEL10:11;
hence thesis by YELLOW_0:60;
end;
f is_>=_than {};
then f = "\/"({}, L) by A1,YELLOW_0:30;
hence thesis by YELLOW_0:def 11;
end;
theorem
for S being non empty RelStr, T being upper-bounded antisymmetric
reflexive non empty RelStr holds Top MonMaps(S, T) = S --> Top T
proof
let S be non empty RelStr, T be upper-bounded antisymmetric reflexive non
empty RelStr;
set L = MonMaps(S, T);
reconsider f = S --> Top T as Element of L by WAYBEL10:9;
reconsider f9 = f as Function of S, T;
A1: for b being Element of L st b is_<=_than {} holds f >= b
proof
let b be Element of L;
assume b is_<=_than {};
reconsider b9 = b as Function of S, T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of T|^ the carrier of S by
YELLOW_0:58;
for x being Element of S holds f9.x >= b9.x
proof
let x be Element of S;
f9. x = ((the carrier of S) --> Top T). x .= Top T by FUNCOP_1:7;
hence thesis by YELLOW_0:45;
end;
then f9 >= b9 by YELLOW_2:9;
then f99 >= b99 by WAYBEL10:11;
hence thesis by YELLOW_0:60;
end;
f is_<=_than {};
then f = "/\"({}, L) by A1,YELLOW_0:31;
hence thesis by YELLOW_0:def 12;
end;
scheme
FuncFraenkelSL{ B, C() -> non empty RelStr, A(set) -> Element of C(), f() ->
Function, P[set]}: f().:{A(x) where x is Element of B(): P[x]} = {f().A(x)
where x is Element of B(): P[x]}
provided
A1: the carrier of C() c= dom f()
proof
set f = f();
thus f.:{A(x) where x is Element of B(): P[x]} c= {f.A(x) where x is Element
of B(): P[x]}
proof
let y be object;
assume y in f.:{A(x) where x is Element of B(): P[x]};
then consider z being object such that
z in dom f and
A2: z in {A(x) where x is Element of B(): P[x]} and
A3: y = f.z by FUNCT_1:def 6;
ex x being Element of B() st z = A(x) & P[x] by A2;
hence thesis by A3;
end;
let y be object;
assume y in {f.A(x) where x is Element of B(): P[x]};
then consider x being Element of B() such that
A4: y = f.A(x) and
A5: P[x];
A(x) in the carrier of C() & A(x) in {A(z) where z is Element of B(): P[
z]} by A5;
hence thesis by A1,A4,FUNCT_1:def 6;
end;
scheme
Fraenkel6A{ B() -> LATTICE, F(set) -> set, P[set], Q[set] } : { F(v1) where
v1 is Element of B() : P[v1] } = { F(v2) where v2 is Element of B() : Q[v2] }
provided
A1: for v being Element of B() holds P[v] iff Q[v]
proof
thus { F(v1) where v1 is Element of B() : P[v1] } c= { F(v2) where v2 is
Element of B() : Q[v2] }
proof
let a be object;
assume a in { F(v1) where v1 is Element of B() : P[v1] };
then consider V1 being Element of B() such that
A2: a = F(V1) and
A3: P[V1];
Q[V1] by A1,A3;
hence thesis by A2;
end;
thus { F(v2) where v2 is Element of B() : Q[v2] } c= { F(v1) where v1 is
Element of B() : P[v1] }
proof
let a be object;
assume a in { F(v1) where v1 is Element of B() : Q[v1] };
then consider V1 being Element of B() such that
A4: a = F(V1) and
A5: Q[V1];
P[V1] by A1,A5;
hence thesis by A4;
end;
end;
theorem Th4:
for S, T being complete LATTICE, f being monotone Function of S,
T holds for x being Element of S holds f.x = sup (f.:downarrow x)
proof
let S, T be complete LATTICE, f be monotone Function of S, T;
let x be Element of S;
A1: for b being Element of T st b is_>=_than f.:downarrow x holds f.x <= b
proof
let b be Element of T;
x <= x;
then dom f = the carrier of S & x in downarrow x by FUNCT_2:def 1
,WAYBEL_0:17;
then
A2: f.x in f.:downarrow x by FUNCT_1:def 6;
assume b is_>=_than f.:downarrow x;
hence thesis by A2;
end;
ex_sup_of downarrow x, S & sup downarrow x = x by WAYBEL_0:34;
then downarrow x is_<=_than x by YELLOW_0:30;
then f.:downarrow x is_<=_than f.x by YELLOW_2:14;
hence thesis by A1,YELLOW_0:30;
end;
theorem
for S, T being complete lower-bounded LATTICE, f being monotone
Function of S, T holds for x being Element of S holds f.x = "\/"({ f.w where w
is Element of S : w <= x },T)
proof
let S, T be complete lower-bounded LATTICE;
let f be monotone Function of S, T;
let x be Element of S;
deffunc A(Element of S) = $1;
defpred P[Element of S] means $1 <= x;
defpred R[Element of S] means ex y1 being Element of S st $1 <= y1 & y1 in {
x};
A1: the carrier of S c= dom f by FUNCT_2:def 1;
A2: f.:{ A(w) where w is Element of S: P[w]} = {f.A(w) where w is Element of
S: P[w]} from FuncFraenkelSL(A1);
A3: for x2 be Element of S holds P[x2] iff R[x2]
proof
let x2 be Element of S;
hereby
A4: x in {x} by TARSKI:def 1;
assume x2 <= x;
hence ex y1 being Element of S st x2 <= y1 & y1 in {x} by A4;
end;
given y1 being Element of S such that
A5: x2 <= y1 & y1 in {x};
thus thesis by A5,TARSKI:def 1;
end;
{ A(w) where w is Element of S : P[w]} = {A(x1) where x1 is Element of S
: R[x1]} from Fraenkel6A (A3);
then
A6: downarrow x = { w where w is Element of S : w <= x } by WAYBEL_0:14;
sup (f.:downarrow x) = f. x by Th4
.= f.sup downarrow x by WAYBEL_0:34;
hence thesis by A2,A6,WAYBEL_0:34;
end;
theorem Th6:
for S being RelStr, T being non empty RelStr, F being Subset of (
T |^ the carrier of S) holds sup F is Function of S, T
proof
let S be RelStr, T be non empty RelStr;
let F be Subset of (T |^ the carrier of S);
set f = sup F;
f in the carrier of (T |^ the carrier of S);
then f in Funcs (the carrier of S, the carrier of T) by YELLOW_1:28;
then ex f9 being Function st f9 = f & dom f9 = the carrier of S & rng f9 c=
the carrier of T by FUNCT_2:def 2;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
begin :: On the Scott continuity of maps
definition
let X1, X2, Y be non empty RelStr;
let f be Function of [:X1, X2:], Y;
let x be Element of X1;
func Proj (f, x) -> Function of X2, Y equals
(curry f).x;
correctness
proof
[:the carrier of X1, the carrier of X2:] = the carrier of [:X1, X2:]
by YELLOW_3:def 2;
then
curry f is Function of the carrier of X1, Funcs(the carrier of X2, the
carrier of Y) by FUNCT_5:67;
hence thesis by FUNCT_2:5,66;
end;
end;
reserve X1, X2, Y for non empty RelStr,
f for Function of [:X1, X2:], Y,
x for Element of X1,
y for Element of X2;
theorem Th7:
for y being Element of X2 holds (Proj (f, x)). y = f.(x, y)
proof
let y be Element of X2;
dom f = the carrier of [:X1, X2:] by FUNCT_2:def 1
.= [:the carrier of X1, the carrier of X2:] by YELLOW_3:def 2;
then [x,y] in dom f by ZFMISC_1:87;
hence thesis by FUNCT_5:20;
end;
definition
let X1, X2, Y be non empty RelStr;
let f be Function of [:X1, X2:], Y;
let y be Element of X2;
func Proj (f, y) -> Function of X1, Y equals
(curry' f).y;
correctness
proof
[:the carrier of X1, the carrier of X2:] = the carrier of [:X1, X2:]
by YELLOW_3:def 2;
then curry' f is Function of the carrier of X2, Funcs(the carrier of X1,
the carrier of Y) by FUNCT_5:68;
hence thesis by FUNCT_2:5,66;
end;
end;
theorem Th8:
for x being Element of X1 holds (Proj (f, y)). x = f.(x, y)
proof
let x be Element of X1;
dom f = the carrier of [:X1, X2:] by FUNCT_2:def 1
.= [:the carrier of X1, the carrier of X2:] by YELLOW_3:def 2;
then [x,y] in dom f by ZFMISC_1:87;
hence thesis by FUNCT_5:22;
end;
theorem Th9:
for R, S, T being non empty RelStr, f being Function of [:R,S:],
T, a being Element of R, b being Element of S holds Proj (f, a). b = Proj (f, b
). a
proof
let R, S, T be non empty RelStr, f be Function of [:R,S:], T, a be Element
of R, b be Element of S;
Proj (f, a). b = f.(a, b) by Th7
.= Proj (f, b). a by Th8;
hence thesis;
end;
registration
let S be non empty RelStr, T be non empty reflexive RelStr;
cluster antitone for Function of S, T;
existence
proof
set c = the Element of T;
take f = S --> c;
let x, y be Element of S;
assume [x, y] in the InternalRel of S;
let a, b be Element of T;
assume that
A1: a = f.x and
A2: b = f.y;
a = c by A1,FUNCOP_1:7;
hence b <= a by A2,FUNCOP_1:7;
end;
end;
theorem Th10:
for R, S, T being non empty reflexive RelStr, f being Function
of [:R,S:], T, a being Element of R, b being Element of S st f is monotone
holds Proj (f, a) is monotone & Proj (f, b) is monotone
proof
let R, S, T be non empty reflexive RelStr, f be Function of [:R,S:], T;
let a be Element of R, b be Element of S;
reconsider a as Element of R;
reconsider b as Element of S;
set g = Proj (f, b), h = Proj (f, a);
assume
A1: f is monotone;
A2: now
let x, y be Element of R;
A3: b <= b;
A4: g. x = f.(x, b) & g. y = f.(y, b) by Th8;
assume x <= y;
then [x, b] <= [y, b] by A3,YELLOW_3:11;
hence g.x <= g.y by A1,A4,WAYBEL_1:def 2;
end;
now
let x, y be Element of S;
A5: a <= a;
A6: h. x = f.(a, x) & h. y = f.(a, y) by Th7;
assume x <= y;
then [a, x] <= [a, y] by A5,YELLOW_3:11;
hence h.x <= h.y by A1,A6,WAYBEL_1:def 2;
end;
hence thesis by A2,WAYBEL_1:def 2;
end;
theorem Th11:
for R, S, T being non empty reflexive RelStr, f being Function
of [:R,S:], T, a being Element of R, b being Element of S st f is antitone
holds Proj (f, a) is antitone & Proj (f, b) is antitone
proof
let R, S, T be non empty reflexive RelStr, f be Function of [:R,S:], T;
let a be Element of R, b be Element of S;
reconsider a9 = a as Element of R;
set g = Proj (f, b), h = Proj (f, a);
assume
A1: f is antitone;
A2: now
reconsider b9 = b as Element of S;
let x, y be Element of R;
A3: b9 <= b9;
A4: g. x = f.(x, b) & g. y = f.(y, b) by Th8;
assume x <= y;
then [x, b9] <= [y, b9] by A3,YELLOW_3:11;
hence g.x >= g.y by A1,A4;
end;
now
let x, y be Element of S;
A5: a9 <= a9;
A6: h. x = f.(a, x) & h. y = f.(a, y) by Th7;
assume x <= y;
then [a9, x] <= [a9, y] by A5,YELLOW_3:11;
hence h.x >= h.y by A1,A6;
end;
hence thesis by A2;
end;
registration
let R, S, T be non empty reflexive RelStr;
let f be monotone Function of [:R, S:], T;
let a be Element of R;
cluster Proj (f, a) -> monotone;
coherence by Th10;
end;
registration
let R, S, T be non empty reflexive RelStr;
let f be monotone Function of [:R, S:], T;
let b be Element of S;
cluster Proj (f, b) -> monotone;
coherence by Th10;
end;
registration
let R, S, T be non empty reflexive RelStr;
let f be antitone Function of [:R, S:], T;
let a be Element of R;
cluster Proj (f, a) -> antitone;
coherence by Th11;
end;
registration
let R, S, T be non empty reflexive RelStr;
let f be antitone Function of [:R, S:], T;
let b be Element of S;
cluster Proj (f, b) -> antitone;
coherence by Th11;
end;
theorem Th12:
for R, S, T being LATTICE, f being Function of [:R,S:], T st (
for a being Element of R, b being Element of S holds Proj (f, a) is monotone &
Proj (f, b) is monotone) holds f is monotone
proof
let R, S, T be LATTICE, f be Function of [:R,S:], T;
assume
A1: for a being Element of R, b being Element of S holds Proj (f, a) is
monotone & Proj (f, b) is monotone;
now
let x, y be Element of [:R, S:];
assume
A2: x <= y;
then
A3: x`1 <= y`1 by YELLOW_3:12;
A4: x`2 <= y`2 by A2,YELLOW_3:12;
A5: f.(x`1, y`2) = Proj (f, x`1). y`2 by Th7;
Proj (f, x`1) is monotone & f.(x`1, x`2) = Proj (f, x`1). x`2 by A1,Th7;
then
A6: f. [x`1, x`2] <= f. [x`1, y`2] by A4,A5,WAYBEL_1:def 2;
A7: f.(y`1, y`2) = Proj (f, y`2). y`1 by Th8;
Proj (f, y`2) is monotone & f.(x`1, y`2) = Proj (f, y`2). x`1 by A1,Th8;
then f. [x`1, y`2] <= f. [y`1, y`2] by A3,A7,WAYBEL_1:def 2;
then
A8: f. [x`1, x`2] <= f. [y`1, y`2] by A6,YELLOW_0:def 2;
A9: [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by
YELLOW_3:def 2;
then f. [y`1, y`2] = f. y by MCART_1:21;
hence f.x <= f.y by A8,A9,MCART_1:21;
end;
hence thesis by WAYBEL_1:def 2;
end;
theorem
for R, S, T being LATTICE, f being Function of [:R,S:], T st ( for a
being Element of R, b being Element of S holds Proj (f, a) is antitone & Proj (
f, b) is antitone) holds f is antitone
proof
let R, S, T be LATTICE, f be Function of [:R,S:], T;
assume
A1: for a being Element of R, b being Element of S holds Proj (f, a) is
antitone & Proj (f, b) is antitone;
now
let x, y be Element of [:R, S:];
assume
A2: x <= y;
then
A3: x`1 <= y`1 by YELLOW_3:12;
A4: x`2 <= y`2 by A2,YELLOW_3:12;
A5: f.(x`1, y`2) = Proj (f, x`1). y`2 by Th7;
Proj (f, x`1) is antitone & f.(x`1, x`2) = Proj (f, x`1). x`2 by A1,Th7;
then
A6: f. [x`1, x`2] >= f. [x`1, y`2] by A4,A5;
A7: f.(y`1, y`2) = Proj (f, y`2). y`1 by Th8;
Proj (f, y`2) is antitone & f.(x`1, y`2) = Proj (f, y`2). x`1 by A1,Th8;
then f. [x`1, y`2] >= f. [y`1, y`2] by A3,A7;
then
A8: f. [x`1, x`2] >= f. [y`1, y`2] by A6,YELLOW_0:def 2;
A9: [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by
YELLOW_3:def 2;
then f. [y`1, y`2] = f. y by MCART_1:21;
hence f.x >= f.y by A8,A9,MCART_1:21;
end;
hence thesis;
end;
theorem Th14:
for R, S, T being LATTICE, f being Function of [:R,S:], T, b
being Element of S, X being Subset of R holds Proj (f, b).:X = f.:[:X, {b}:]
proof
let R, S, T be LATTICE, f be Function of [:R,S:], T, b be Element of S, X be
Subset of R;
A1: Proj (f, b).:X c= f.:[:X, {b}:]
proof
let c be object;
assume c in Proj (f, b).:X;
then consider k be object such that
A2: k in dom Proj (f, b) and
A3: k in X and
A4: c = Proj (f, b).k by FUNCT_1:def 6;
b in {b} by TARSKI:def 1;
then
A5: [k, b] in [:X, {b}:] by A3,ZFMISC_1:87;
[:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by
YELLOW_3:def 2;
then dom f = [:the carrier of R, the carrier of S:] by FUNCT_2:def 1;
then
A6: [k, b] in dom f by A2,ZFMISC_1:87;
c = f.(k, b) by A2,A4,Th8;
hence thesis by A5,A6,FUNCT_1:def 6;
end;
f.:[:X, {b}:] c= Proj (f, b).:X
proof
let c be object;
assume c in f.:[:X, {b}:];
then consider k be object such that
k in dom f and
A7: k in [:X, {b}:] and
A8: c = f.k by FUNCT_1:def 6;
consider k1, k2 be object such that
A9: k1 in X and
A10: k2 in {b} and
A11: k = [k1, k2] by A7,ZFMISC_1:def 2;
A12: k2 = b by A10,TARSKI:def 1;
c = f.(k1,k2) by A8,A11;
then dom Proj (f, b) = the carrier of R & c = Proj (f, b). k1 by A9,A12,Th8
,FUNCT_2:def 1;
hence thesis by A9,FUNCT_1:def 6;
end;
hence thesis by A1;
end;
theorem Th15:
for R, S, T being LATTICE, f being Function of [:R,S:], T, b
being Element of R, X being Subset of S holds Proj (f, b).:X = f.:[:{b}, X:]
proof
let R, S, T be LATTICE, f be Function of [:R,S:], T, b be Element of R, X be
Subset of S;
A1: Proj (f, b).:X c= f.:[:{b}, X:]
proof
let c be object;
assume c in Proj (f, b).:X;
then consider k be object such that
A2: k in dom Proj (f, b) and
A3: k in X and
A4: c = Proj (f, b).k by FUNCT_1:def 6;
b in {b} by TARSKI:def 1;
then
A5: [b, k] in [:{b}, X:] by A3,ZFMISC_1:87;
[:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by
YELLOW_3:def 2;
then dom f = [:the carrier of R, the carrier of S:] by FUNCT_2:def 1;
then
A6: [b, k] in dom f by A2,ZFMISC_1:87;
c = f.(b, k) by A2,A4,Th7;
hence thesis by A5,A6,FUNCT_1:def 6;
end;
f.:[:{b}, X:] c= Proj (f, b).:X
proof
let c be object;
assume c in f.:[:{b}, X:];
then consider k be object such that
k in dom f and
A7: k in [:{b}, X:] and
A8: c = f.k by FUNCT_1:def 6;
consider k1, k2 be object such that
A9: k1 in {b} and
A10: k2 in X and
A11: k = [k1, k2] by A7,ZFMISC_1:def 2;
A12: k1 = b by A9,TARSKI:def 1;
c = f.(k1,k2) by A8,A11;
then dom Proj (f, b) = the carrier of S & c = Proj (f, b). k2 by A10,A12
,Th7,FUNCT_2:def 1;
hence thesis by A10,FUNCT_1:def 6;
end;
hence thesis by A1;
end;
theorem :: Lemma 2.9 p. 116 (1) => (2)
for R, S, T being LATTICE, f being Function of [:R,S:], T, a being
Element of R, b being Element of S st f is directed-sups-preserving holds Proj
(f, a) is directed-sups-preserving & Proj (f, b) is directed-sups-preserving
proof
let R, S, T be LATTICE, f be Function of [:R,S:], T, a be Element of R, b be
Element of S;
assume
A1: f is directed-sups-preserving;
A2: for X being Subset of S st X is non empty directed holds Proj (f, a)
preserves_sup_of X
proof
reconsider Y9 = {a} as non empty directed Subset of R by WAYBEL_0:5;
let X be Subset of S;
assume X is non empty directed;
then reconsider X9 = X as non empty directed Subset of S;
Proj (f, a) preserves_sup_of X
proof
A3: sup Y9 = a by YELLOW_0:39;
A4: f preserves_sup_of [:Y9, X9:] by A1;
A5: Proj (f, a).:X = f.:[:Y9, X9:] by Th15;
A6: ex_sup_of Y9, R by YELLOW_0:38;
assume
A7: ex_sup_of X, S;
then
A8: ex_sup_of [:Y9, X9:], [:R, S:] by A6,YELLOW_3:39;
sup (Proj (f, a).:X) = sup (f.:[:Y9, X9:]) by Th15
.= f.(sup [:Y9, X9:]) by A8,A4
.= f.(sup Y9, sup X9) by A7,A6,YELLOW_3:43
.= Proj (f, a).sup X by A3,Th7;
hence thesis by A8,A4,A5;
end;
hence thesis;
end;
for X being Subset of R st X is non empty directed holds Proj (f, b)
preserves_sup_of X
proof
reconsider Y9 = {b} as non empty directed Subset of S by WAYBEL_0:5;
let X be Subset of R;
assume X is non empty directed;
then reconsider X9 = X as non empty directed Subset of R;
Proj (f, b) preserves_sup_of X
proof
A9: sup Y9 = b by YELLOW_0:39;
A10: f preserves_sup_of [:X9, Y9:] by A1;
A11: Proj (f, b).:X = f.:[:X9, Y9:] by Th14;
A12: ex_sup_of Y9, S by YELLOW_0:38;
assume
A13: ex_sup_of X, R;
then
A14: ex_sup_of [:X9, Y9:], [:R, S:] by A12,YELLOW_3:39;
sup (Proj (f, b).:X) = sup (f.:[:X9, Y9:]) by Th14
.= f.(sup [:X9, Y9:]) by A14,A10
.= f.(sup X9, sup Y9) by A13,A12,YELLOW_3:43
.= Proj (f, b).sup X by A9,Th8;
hence thesis by A14,A10,A11;
end;
hence thesis;
end;
hence thesis by A2;
end;
theorem Th17:
for R, S, T being LATTICE, f being monotone Function of [:R, S:]
, T, a being Element of R, b being Element of S, X being directed Subset of [:R
, S:] st ex_sup_of f.:X, T & a in proj1 X & b in proj2 X holds f. [a, b] <= sup
(f.:X)
proof
let R, S, T be LATTICE, f be monotone Function of [:R, S:], T, a be Element
of R, b be Element of S, X be directed Subset of [:R, S:];
assume that
A1: ex_sup_of f.:X, T and
A2: a in proj1 X and
A3: b in proj2 X;
consider d being object such that
A4: [d, b] in X by A3,XTUPLE_0:def 13;
d in proj1 X by A4,XTUPLE_0:def 12;
then reconsider d as Element of R;
consider c being object such that
A5: [a, c] in X by A2,XTUPLE_0:def 12;
c in proj2 X by A5,XTUPLE_0:def 13;
then reconsider c as Element of S;
consider z being Element of [:R, S:] such that
A6: z in X and
A7: [a, c] <= z & [d, b] <= z by A5,A4,WAYBEL_0:def 1;
A8: f.:X is_<=_than sup (f.:X) by A1,YELLOW_0:30;
[a, c] "\/" [d, b] <= z "\/" z by A7,YELLOW_3:3;
then [a, c] "\/" [d, b] <= z by YELLOW_5:1;
then [a "\/" d, c "\/" b] <= z by YELLOW10:16;
then
A9: f. [a "\/" d, c "\/" b] <= f. z by WAYBEL_1:def 2;
dom f = the carrier of [:R, S:] by FUNCT_2:def 1;
then f.z in f.:X by A6,FUNCT_1:def 6;
then
A10: f. z <= sup (f.:X) by A8;
a <= a "\/" d & b <= c "\/" b by YELLOW_0:22;
then [a, b] <= [a "\/" d, c "\/" b] by YELLOW_3:11;
then f. [a, b] <= f. [a "\/" d, c "\/" b] by WAYBEL_1:def 2;
then f. [a, b] <= f. z by A9,YELLOW_0:def 2;
hence thesis by A10,YELLOW_0:def 2;
end;
theorem :: Lemma 2.9 p. 116 (2) => (1)
for R, S, T being complete LATTICE, f being Function of [:R, S:], T st
( for a being Element of R, b being Element of S holds Proj (f, a) is
directed-sups-preserving & Proj (f, b) is directed-sups-preserving ) holds f is
directed-sups-preserving
proof
let R, S, T be complete LATTICE, f be Function of [:R,S:], T;
assume
A1: for a being Element of R, b being Element of S holds Proj (f, a) is
directed-sups-preserving & Proj (f, b) is directed-sups-preserving;
for X being Subset of [:R, S:] st X is non empty directed holds f
preserves_sup_of X
proof
let X be Subset of [:R, S:];
assume X is non empty directed;
then reconsider X as non empty directed Subset of [:R, S:];
for a be Element of R, b be Element of S holds Proj (f, a) is monotone
& Proj (f, b) is monotone by A1,WAYBEL17:3;
then
A2: f is monotone by Th12;
f preserves_sup_of X
proof
proj1 X is directed non empty & Proj (f, "\/"(proj2 X, S)) is
directed-sups-preserving by A1,YELLOW_3:21,22;
then
A3: Proj (f, "\/"(proj2 X, S)) preserves_sup_of proj1 X;
A4: ex_sup_of (Proj (f, sup proj2 X).:proj1 X), T by YELLOW_0:17;
assume
A5: ex_sup_of X, [:R, S:];
then
A6: ex_sup_of proj1 X, R by YELLOW_3:41;
A7: ex_sup_of proj2 X, S by A5,YELLOW_3:41;
for b being Element of T st b in Proj (f, sup proj2 X).:proj1 X
holds b <= sup (f.:X)
proof
let b be Element of T;
assume b in Proj (f, sup proj2 X).:proj1 X;
then consider b1 being object such that
A8: b1 in dom Proj (f, sup proj2 X) and
A9: b1 in proj1 X and
A10: b = (Proj (f, sup proj2 X)).b1 by FUNCT_1:def 6;
reconsider b1 as Element of R by A8;
A11: (Proj (f, b1).:proj2 X) is_<=_than sup (f.:X)
proof
let k be Element of T;
assume k in (Proj (f, b1).:proj2 X);
then consider k1 being object such that
A12: k1 in dom Proj (f, b1) and
A13: k1 in proj2 X and
A14: k = (Proj (f, b1)).k1 by FUNCT_1:def 6;
reconsider k1 as Element of S by A12;
k = f.(b1, k1) by A14,Th7;
hence thesis by A2,A9,A13,Th17,YELLOW_0:17;
end;
proj2 X is non empty directed & Proj (f, b1) is
directed-sups-preserving by A1,YELLOW_3:21,22;
then
A15: Proj (f, b1) preserves_sup_of proj2 X;
A16: ex_sup_of (Proj (f, b1).:proj2 X), T by YELLOW_0:17;
b = (Proj (f, b1)). sup proj2 X by A10,Th9
.= sup (Proj (f, b1).:proj2 X) by A7,A15;
hence thesis by A16,A11,YELLOW_0:def 9;
end;
then
A17: Proj (f, sup proj2 X).:proj1 X is_<=_than sup (f.:X);
A18: sup (f.:X) <= f.sup X by A2,WAYBEL17:16;
f.sup X = f.(sup proj1 X, sup proj2 X) by YELLOW_3:46
.= Proj (f, sup proj2 X). sup proj1 X by Th8
.= sup (Proj (f, sup proj2 X).:proj1 X) by A6,A3;
then f.sup X <= sup (f.:X) by A17,A4,YELLOW_0:def 9;
hence thesis by A18,YELLOW_0:17,def 3;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th19:
for S being set, T being non empty RelStr, f be set holds f is
Element of T |^ S iff f is Function of S, the carrier of T
proof
let S be set, T be non empty RelStr, f be set;
hereby
assume f is Element of (T |^ S);
then f in the carrier of (T |^ S);
then f in Funcs (S, the carrier of T) by YELLOW_1:28;
then
ex a being Function st a = f & dom a = S & rng a c= the carrier of T by
FUNCT_2:def 2;
hence f is Function of S, the carrier of T by FUNCT_2:def 1,RELSET_1:4;
end;
assume f is Function of S, the carrier of T;
then f in Funcs (S, the carrier of T) by FUNCT_2:8;
hence thesis by YELLOW_1:28;
end;
begin :: The poset of continuous maps
definition
let S be TopStruct, T be non empty TopRelStr;
func ContMaps (S, T) -> strict RelStr means
:Def3:
it is full SubRelStr of T
|^ the carrier of S & for x being set holds x in the carrier of it iff ex f
being Function of S, T st x = f & f is continuous;
existence
proof
defpred P[object] means
ex f be Function of S, T st $1 = f & f is continuous;
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;
hereby
assume f in the carrier of SX;
then f in X by YELLOW_0:def 15;
then consider f9 be Function of S, T such that
A2: f9 = f & f9 is continuous by A1;
take f9;
thus f9 = f & f9 is continuous by A2;
end;
given f9 being Function of S, T such that
A3: f = f9 and
A4: f9 is continuous;
f in Funcs (the carrier of S, the carrier of T) by A3,FUNCT_2:8;
then f in the carrier of (T |^ the carrier of S) by YELLOW_1:28;
then f in X by A1,A3,A4;
hence thesis by YELLOW_0:def 15;
end;
uniqueness
proof
let A1, A2 be strict RelStr;
assume that
A5: A1 is full SubRelStr of T |^ the carrier of S and
A6: for x being set holds x in the carrier of A1 iff ex f being
Function of S, T st x = f & f is continuous and
A7: A2 is full SubRelStr of T |^ the carrier of S and
A8: for x being set holds x in the carrier of A2 iff ex f being
Function of S, T st x = f & f is continuous;
the carrier of A1 = the carrier of A2
proof
hereby
let x be object;
assume x in the carrier of A1;
then ex f being Function of S, T st x = f & f is continuous by A6;
hence x in the carrier of A2 by A8;
end;
let x be object;
assume x in the carrier of A2;
then ex f being Function of S, T st x = f & f is continuous by A8;
hence thesis by A6;
end;
hence thesis by A5,A7,YELLOW_0:57;
end;
end;
registration
let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> non empty;
coherence
proof
set f = the continuous Function of S, T;
f in the carrier of ContMaps(S,T) by Def3;
hence thesis;
end;
end;
registration
let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> constituted-Functions;
coherence
proof
let a be Element of ContMaps (S, T);
ex a9 being Function of S, T st a9 = a & a9 is continuous by Def3;
hence thesis;
end;
end;
theorem Th20:
for S being non empty TopSpace, T being non empty reflexive
TopSpace-like TopRelStr, x, y being Element of ContMaps (S, T) holds x <= y iff
for i being Element of S holds [x.i, y.i] in the InternalRel of T
proof
let S be non empty TopSpace, T be non empty reflexive TopSpace-like
TopRelStr, x, y be Element of ContMaps (S, T);
A1: ContMaps (S, T) is full SubRelStr of T |^ the carrier of S by Def3;
then reconsider x9 = x, y9 = y as Element of (T |^ the carrier of S) by
YELLOW_0:58;
reconsider xa = x9, ya = y9 as Function of S, T by Th19;
hereby
assume
A2: x <= y;
let i be Element of S;
x9 <= y9 by A1,A2,YELLOW_0:59;
then xa <= ya by WAYBEL10:11;
then ex a, b being Element of T st a = xa.i & b = ya.i & a <= b by
YELLOW_2:def 1;
hence [x.i, y.i] in the InternalRel of T;
end;
assume
A3: for i being Element of S holds [x.i, y.i] in the InternalRel of T;
now
let j be set;
assume j in the carrier of S;
then reconsider i = j as Element of S;
reconsider a = xa.i, b = ya.i as Element of T;
take a, b;
thus a = xa.j & b = ya.j;
[a, b] in the InternalRel of T by A3;
hence a <= b;
end;
then xa <= ya by YELLOW_2:def 1;
then x9 <= y9 by WAYBEL10:11;
hence thesis by A1,YELLOW_0:60;
end;
theorem Th21:
for S being non empty TopSpace, T being non empty reflexive
TopSpace-like TopRelStr, x being set holds x is continuous Function of S, T iff
x is Element of ContMaps (S, T)
proof
let S be non empty TopSpace, T be non empty reflexive TopSpace-like
TopRelStr, x be set;
thus x is continuous Function of S, T implies x is Element of ContMaps (S, T
) by Def3;
assume x is Element of ContMaps (S, T);
then ex f being Function of S, T st x = f & f is continuous by Def3;
hence thesis;
end;
registration
let S be non empty TopSpace, T be non empty reflexive TopSpace-like
TopRelStr;
cluster ContMaps (S, T) -> reflexive;
coherence
proof
reconsider CS = ContMaps (S, T) as full SubRelStr of T |^ the carrier of S
by Def3;
CS is reflexive;
hence thesis;
end;
end;
registration
let S be non empty TopSpace, T be non empty transitive TopSpace-like
TopRelStr;
cluster ContMaps (S, T) -> transitive;
coherence
proof
reconsider CS = ContMaps (S, T) as full SubRelStr of T |^ the carrier of S
by Def3;
CS is transitive;
hence thesis;
end;
end;
registration
let S be non empty TopSpace, T be non empty antisymmetric TopSpace-like
TopRelStr;
cluster ContMaps (S, T) -> antisymmetric;
coherence
proof
reconsider CS = ContMaps (S, T) as full SubRelStr of T |^ the carrier of S
by Def3;
CS is antisymmetric;
hence thesis;
end;
end;
registration
let S be set, T be non empty RelStr;
cluster T |^ S -> constituted-Functions;
coherence
by Th19;
end;
theorem
for S being non empty 1-sorted, T being complete LATTICE for f, g, h
being Function of S, T, i being Element of S st h = "\/" ({f, g}, T |^ the
carrier of S) holds h.i = sup {f.i, g.i}
proof
let S be non empty 1-sorted, T be complete LATTICE;
let f, g, h be Function of S, T, i be Element of S;
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
reconsider SYT = (the carrier of S) --> T as non-Empty RelStr-yielding
ManySortedSet of the carrier of S;
reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet
of the carrier of S;
A1: for i being Element of S holds SYT.i is complete LATTICE by FUNCOP_1:7;
reconsider f9, g9 as Element of product SYT by YELLOW_1:def 5;
reconsider DU = {f9, g9} as Subset of product SYT;
assume h = "\/" ({f, g}, T |^ the carrier of S);
then h.i = (sup DU).i by YELLOW_1:def 5
.= "\/" (pi({f,g},i), SYT.i) by A1,WAYBEL_3:32
.= "\/" (pi({f,g},i), T) by FUNCOP_1:7
.= sup {f.i, g.i} by CARD_3:15;
hence thesis;
end;
theorem Th23:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
complete LATTICE for X being Subset of product J, i being Element of I holds (
inf X).i = inf pi(X,i)
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds J.i is complete LATTICE;
then reconsider L = product J as complete LATTICE by WAYBEL_3:31;
let X be Subset of product J, i be Element of I;
A2: L is complete;
then
A3: inf X is_<=_than X by YELLOW_0:33;
A4: (inf X).i is_<=_than pi(X,i)
proof
let a be Element of J.i;
assume a in pi(X,i);
then consider f being Function such that
A5: f in X and
A6: a = f.i by CARD_3:def 6;
reconsider f as Element of product J by A5;
inf X <= f by A3,A5;
hence thesis by A6,WAYBEL_3:28;
end;
A7: now
let a be Element of J.i;
set f = (inf X)+*(i,a);
A8: dom f = dom inf X by FUNCT_7:30;
A9: dom inf X = I by WAYBEL_3:27;
now
let j be Element of I;
j = i or j <> i;
then f.j = (inf X).j or f.j = a & j = i by A9,FUNCT_7:31,32;
hence f.j is Element of J.j;
end;
then reconsider f as Element of product J by A8,WAYBEL_3:27;
assume
A10: a is_<=_than pi(X,i);
f is_<=_than X
proof
let g be Element of product J;
assume g in X;
then
A11: g >= inf X & g.i in pi(X,i) by A2,CARD_3:def 6,YELLOW_2:22;
now
let j be Element of I;
j = i or j <> i;
then f.j = (inf X).j or f.j = a & j = i by A9,FUNCT_7:31,32;
hence f.j <= g.j by A10,A11,WAYBEL_3:28;
end;
hence f <= g by WAYBEL_3:28;
end;
then
A12: f <= inf X by A2,YELLOW_0:33;
f.i = a by A9,FUNCT_7:31;
hence (inf X).i >= a by A12,WAYBEL_3:28;
end;
J.i is complete LATTICE by A1;
hence thesis by A4,A7,YELLOW_0:33;
end;
theorem
for S being non empty 1-sorted, T being complete LATTICE for f, g, h
being Function of S, T, i being Element of S st h = "/\" ({f, g}, T |^ the
carrier of S) holds h.i = inf {f.i, g.i}
proof
let S be non empty 1-sorted, T be complete LATTICE;
let f, g, h be Function of S, T, i be Element of S;
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
reconsider SYT = (the carrier of S) --> T as non-Empty RelStr-yielding
ManySortedSet of the carrier of S;
reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet
of the carrier of S;
A1: for i being Element of S holds SYT.i is complete LATTICE by FUNCOP_1:7;
reconsider f9, g9 as Element of product SYT by YELLOW_1:def 5;
reconsider DU = {f9, g9} as Subset of product SYT;
assume h = "/\" ({f, g}, T |^ the carrier of S);
then h.i = (inf DU).i by YELLOW_1:def 5
.= "/\" (pi({f,g},i), SYT.i) by A1,Th23
.= "/\" (pi({f,g},i), T) by FUNCOP_1:7
.= inf {f.i, g.i} by CARD_3:15;
hence thesis;
end;
theorem Th25:
for S being non empty RelStr, T being complete LATTICE for F
being non empty Subset of (T |^ the carrier of S), i being Element of S holds (
sup F).i = "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }
, T )
proof
let S be non empty RelStr, T be complete LATTICE;
let F be non empty Subset of (T |^ the carrier of S), i be Element of S;
reconsider SYT = (the carrier of S) --> T as non-Empty RelStr-yielding
ManySortedSet of the carrier of S;
reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet
of the carrier of S;
reconsider X = F as Subset of product SYT by YELLOW_1:def 5;
A1: pi(X,i) = { f.i where f is Element of (T |^ the carrier of S) : f in F }
proof
thus pi(X,i) c= { f.i where f is Element of (T |^ the carrier of S) : f in
F }
proof
let a be object;
assume a in pi(X,i);
then ex g being Function st g in X & a = g.i by CARD_3:def 6;
hence thesis;
end;
thus { f.i where f is Element of (T |^ the carrier of S) : f in F } c= pi(
X,i)
proof
let a be object;
assume
a in { f.i where f is Element of (T |^ the carrier of S) : f in F };
then
ex g being Element of (T |^ the carrier of S) st a = g.i & g in F;
hence thesis by CARD_3:def 6;
end;
end;
T |^ the carrier of S = product SYT & for i being Element of S holds SYT
.i is complete LATTICE by FUNCOP_1:7,YELLOW_1:def 5;
then (sup F).i = "\/" (pi(X,i), SYT.i) by WAYBEL_3:32
.= "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F },
T ) by A1,FUNCOP_1:7;
hence thesis;
end;
theorem Th26:
for S, T being complete TopLattice for F being non empty Subset
of ContMaps (S, T), i being Element of S holds "\/" (F, (T |^ the carrier of S)
).i = "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T )
proof
let S, T be complete TopLattice;
let F be non empty Subset of ContMaps (S, T), i be Element of S;
reconsider SYT = (the carrier of S) --> T as non-Empty RelStr-yielding
ManySortedSet of the carrier of S;
reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet
of the carrier of S;
ContMaps (S, T) is full SubRelStr of (T |^ the carrier of S) by Def3;
then
the carrier of ContMaps (S, T) c= the carrier of (T |^ the carrier of S
) by YELLOW_0:def 13;
then
A1: F c= the carrier of (T |^ the carrier of S);
then reconsider X = F as Subset of product SYT by YELLOW_1:def 5;
A2: pi(X,i) = { f.i where f is Element of (T |^ the carrier of S) : f in F }
proof
thus pi(X,i) c= { f.i where f is Element of (T |^ the carrier of S) : f in
F }
proof
let a be object;
assume a in pi(X,i);
then ex g being Function st g in X & a = g.i by CARD_3:def 6;
hence thesis by A1;
end;
thus { f.i where f is Element of (T |^ the carrier of S) : f in F } c= pi(
X,i)
proof
let a be object;
assume
a in { f.i where f is Element of (T |^ the carrier of S) : f in F };
then
ex g being Element of (T |^ the carrier of S) st a = g.i & g in F;
hence thesis by CARD_3:def 6;
end;
end;
T |^ the carrier of S = product SYT & for i being Element of S holds SYT
.i is complete LATTICE by FUNCOP_1:7,YELLOW_1:def 5;
then "\/" (F, (T |^ the carrier of S)).i = "\/" (pi(X,i), SYT.i) by
WAYBEL_3:32
.= "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F },
T ) by A2,FUNCOP_1:7;
hence thesis;
end;
reserve S for non empty RelStr,
T for complete LATTICE;
theorem Th27:
for F being non empty Subset of (T |^ the carrier of S), D being
non empty Subset of S holds (sup F).:D = { "\/" ({ f.i where f is Element of (T
|^ the carrier of S) : f in F }, T ) where i is Element of S : i in D }
proof
let F be non empty Subset of (T |^ the carrier of S), D be non empty Subset
of S;
thus (sup F).:D c= { "\/" ({ f.i where f is Element of (T |^ the carrier of
S) : f in F }, T ) where i is Element of S: i in D }
proof
let a be object;
assume a in (sup F).:D;
then consider x being object such that
x in dom (sup F) and
A1: x in D and
A2: a = (sup F).x by FUNCT_1:def 6;
reconsider x9 = x as Element of S by A1;
a = "\/" ({ f.x9 where f is Element of (T |^ the carrier of S) : f in
F }, T ) by A2,Th25;
hence thesis by A1;
end;
thus { "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }
, T ) where i is Element of S: i in D } c= (sup F).:D
proof
sup F is Function of S, T by Th6;
then
A3: dom (sup F) = the carrier of S by FUNCT_2:def 1;
let a be object;
assume a in { "\/" ({ f.i where f is Element of (T |^ the carrier of S) :
f in F }, T ) where i is Element of S: i in D };
then consider i1 being Element of S such that
A4: a = "\/" ({ f.i1 where f is Element of (T |^ the carrier of S) : f
in F }, T ) & i1 in D;
a = (sup F).i1 by A4,Th25;
hence thesis by A4,A3,FUNCT_1:def 6;
end;
end;
theorem Th28:
for S, T being complete Scott TopLattice, F being non empty
Subset of ContMaps (S, T), D being non empty Subset of S holds ("\/" (F, (T |^
the carrier of S))).:D = { "\/" ({ f.i where f is Element of (T |^ the carrier
of S) : f in F }, T ) where i is Element of S : i in D }
proof
let S, T be complete Scott TopLattice, F be non empty Subset of ContMaps (S,
T), D be non empty Subset of S;
thus ("\/" (F, (T |^ the carrier of S))).:D c= { "\/" ({ f.i where f is
Element of (T |^ the carrier of S) : f in F }, T ) where i is Element of S: i
in D }
proof
let a be object;
assume a in ("\/" (F, (T |^ the carrier of S))).:D;
then consider x being object such that
x in dom ("\/" (F, (T |^ the carrier of S))) and
A1: x in D and
A2: a = ("\/" (F, (T |^ the carrier of S))).x by FUNCT_1:def 6;
reconsider x9 = x as Element of S by A1;
a = "\/" ({ f.x9 where f is Element of (T |^ the carrier of S) : f in
F }, T ) by A2,Th26;
hence thesis by A1;
end;
thus { "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }
, T ) where i is Element of S: i in D } c= ("\/" (F, (T |^ the carrier of S)))
.:D
proof
("\/" (F, (T |^ the carrier of S))) is Function of S, T by Th19;
then
A3: dom ("\/" (F, (T |^ the carrier of S))) = the carrier of S by FUNCT_2:def 1
;
let a be object;
assume a in { "\/" ({ f.i where f is Element of (T |^ the carrier of S) :
f in F }, T ) where i is Element of S: i in D };
then consider i1 being Element of S such that
A4: a = "\/" ({ f.i1 where f is Element of (T |^ the carrier of S) : f
in F }, T ) & i1 in D;
a = ("\/" (F, (T |^ the carrier of S))).i1 by A4,Th26;
hence thesis by A4,A3,FUNCT_1:def 6;
end;
end;
scheme
FraenkelF9RS{ B() -> non empty TopRelStr, F(set) -> set, G(set) -> set, P[
set] } : { F(v1) where v1 is Element of B() : P[v1] } = { G(v2) where v2 is
Element of B() : P[v2] }
provided
A1: for v being Element of B() st P[v] holds F(v) = G(v)
proof
set X = { F(v1) where v1 is Element of B() : P[v1] }, Y = { G(v2) where v2
is Element of B() : P[v2] };
A2: Y c= X
proof
let x be object;
assume x in Y;
then consider v1 being Element of B() such that
A3: x = G(v1) and
A4: P[v1];
x = F(v1) by A1,A3,A4;
hence thesis by A4;
end;
X c= Y
proof
let x be object;
assume x in X;
then consider v1 being Element of B() such that
A5: x = F(v1) and
A6: P[v1];
x = G(v1) by A1,A5,A6;
hence thesis by A6;
end;
hence thesis by A2;
end;
scheme
FraenkelF9RSS{ B() -> non empty RelStr, F(set) -> set, G(set) -> set, P[set]
} : { F(v1) where v1 is Element of B() : P[v1] } = { G(v2) where v2 is Element
of B() : P[v2] }
provided
A1: for v being Element of B() st P[v] holds F(v) = G(v)
proof
set X = { F(v1) where v1 is Element of B() : P[v1] }, Y = { G(v2) where v2
is Element of B() : P[v2] };
A2: Y c= X
proof
let x be object;
assume x in Y;
then consider v1 being Element of B() such that
A3: x = G(v1) and
A4: P[v1];
x = F(v1) by A1,A3,A4;
hence thesis by A4;
end;
X c= Y
proof
let x be object;
assume x in X;
then consider v1 being Element of B() such that
A5: x = F(v1) and
A6: P[v1];
x = G(v1) by A1,A5,A6;
hence thesis by A6;
end;
hence thesis by A2;
end;
scheme
FuncFraenkelS{ B, C() -> non empty TopRelStr, A(set) -> Element of C(), f()
-> Function, P[set]}: f().:{A(x) where x is Element of B(): P[x]} = {f().A(x)
where x is Element of B(): P[x]}
provided
A1: the carrier of C() c= dom f()
proof
set f = f();
thus f.:{A(x) where x is Element of B(): P[x]} c= {f.A(x) where x is Element
of B(): P[x]}
proof
let y be object;
assume y in f.:{A(x) where x is Element of B(): P[x]};
then consider z being object such that
z in dom f and
A2: z in {A(x) where x is Element of B(): P[x]} and
A3: y = f.z by FUNCT_1:def 6;
ex x being Element of B() st z = A(x) & P[x] by A2;
hence thesis by A3;
end;
let y be object;
assume y in {f.A(x) where x is Element of B(): P[x]};
then consider x being Element of B() such that
A4: y = f.A(x) and
A5: P[x];
A(x) in the carrier of C() & A(x) in {A(z) where z is Element of B(): P[
z]} by A5;
hence thesis by A1,A4,FUNCT_1:def 6;
end;
Lm1: for S being non empty RelStr, D being non empty Subset of S holds D = { i
where i is Element of S: i in D }
proof
let S be non empty RelStr, D be non empty Subset of S;
thus D c= { i where i is Element of S: i in D };
thus { i where i is Element of S: i in D } c= D
proof
let a be object;
assume a in { i where i is Element of S: i in D };
then ex j being Element of S st j = a & j in D;
hence thesis;
end;
end;
theorem Th29:
for S, T being complete Scott TopLattice, F being non empty
Subset of ContMaps (S, T) holds "\/" (F, (T |^ the carrier of S)) is monotone
Function of S, T
proof
let S, T be complete Scott TopLattice, F be non empty Subset of ContMaps (S,
T);
ContMaps (S, T) is full SubRelStr of (T |^ the carrier of S) by Def3;
then
the carrier of ContMaps (S, T) c= the carrier of (T |^ the carrier of S
) by YELLOW_0:def 13;
then reconsider F9 = F as Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F9 as Function of S, T by Th6;
now
let x, y be Element of S;
set G1 = { f.x where f is Element of (T |^ the carrier of S) : f in F9 };
assume
A1: x <= y;
A2: G1 is_<=_than sF.y
proof
let a be Element of T;
assume
a in { f.x where f is Element of (T |^ the carrier of S) : f in F9 };
then consider f9 being Element of (T |^ the carrier of S) such that
A3: a = f9.x and
A4: f9 in F9;
reconsider f1 = f9 as continuous Function of S, T by A4,Th21;
reconsider f1 as monotone Function of S, T;
f9 <= sup F9 by A4,YELLOW_2:22;
then f1 <= sF by WAYBEL10:11;
then
A5: f1.y <= sF.y by YELLOW_2:9;
f1.x <= f1.y by A1,WAYBEL_1:def 2;
hence thesis by A3,A5,YELLOW_0:def 2;
end;
sF.x = "\/" (G1, T) by Th25;
hence sF.x <= sF.y by A2,YELLOW_0:32;
end;
hence thesis by WAYBEL_1:def 2;
end;
theorem Th30:
for S, T being complete Scott TopLattice, F being non empty
Subset of ContMaps (S, T), D being directed non empty Subset of S holds "\/"({
"\/"({g.i where i is Element of S : i in D }, T ) where g is Element of (T |^
the carrier of S) : g in F }, T ) = "\/"({ "\/" ({g9.i9 where g9 is Element of
(T |^ the carrier of S) : g9 in F }, T ) where i9 is Element of S : i9 in D },
T)
proof
let S, T be complete Scott TopLattice, F be non empty Subset of ContMaps (S,
T), D be directed non empty Subset of S;
reconsider sF = "\/" (F, (T |^ the carrier of S)) as Function of S, T by Th19
;
set F9 = F;
set L = "\/"({ "\/"({g.i where i is Element of S : i in D }, T ) where g is
Element of (T |^ the carrier of S) : g in F }, T );
set P = "\/"({ "\/" ({g9.i9 where g9 is Element of (T |^ the carrier of S) :
g9 in F }, T ) where i9 is Element of S : i9 in D }, T);
set L1 = { "\/"({g.i where i is Element of S : i in D }, T) where g is
Element of (T |^ the carrier of S) : g in F };
set P1 = { "\/"({g2.i3 where g2 is Element of (T |^ the carrier of S) : g2
in F }, T ) where i3 is Element of S : i3 in D };
reconsider L, P as Element of T;
defpred Q[set] means $1 in F9;
deffunc A(Element of S) = $1;
defpred P[set] means $1 in D;
deffunc F(Element of (T |^ the carrier of S)) = "\/"({$1.i4 where i4 is
Element of S : i4 in D }, T );
deffunc G(Element of (T |^ the carrier of S)) = $1.sup D;
A1: P = sup (sF.:D) by Th28;
L1 is_<=_than P
proof
let b be Element of T;
assume b in L1;
then consider g9 being Element of T |^ the carrier of S such that
A2: b = "\/"({g9.i where i is Element of S : i in D }, T) and
A3: g9 in F;
reconsider g1 = g9 as continuous Function of S, T by A3,Th21;
g9 <= "\/" (F, (T |^ the carrier of S)) by A3,YELLOW_2:22;
then
A4: g1 <= sF by WAYBEL10:11;
A5: g1.:D is_<=_than sup (sF.:D)
proof
let a be Element of T;
assume a in g1.:D;
then consider x be object such that
A6: x in dom g1 and
A7: x in D and
A8: a = g1.x by FUNCT_1:def 6;
reconsider x9 = x as Element of S by A6;
x in the carrier of S by A6;
then x9 in dom sF by FUNCT_2:def 1;
then sF.x9 in sF.:D by A7,FUNCT_1:def 6;
then
A9: sF.x9 <= sup (sF.:D) by YELLOW_2:22;
g1.x9 <= sF.x9 by A4,YELLOW_2:9;
hence thesis by A8,A9,YELLOW_0:def 2;
end;
the carrier of S c= dom g1 by FUNCT_2:def 1;
then
A10: the carrier of S c= dom g9;
g9.:{A(i2) where i2 is Element of S : P[i2]} = {g9.A(i) where i is
Element of S : P[i]} from FuncFraenkelS (A10);
then b = "\/" (g9.:D, T) by A2,Lm1;
hence thesis by A1,A5,YELLOW_0:32;
end;
then
A11: L <= P by YELLOW_0:32;
A12: for g8 being Element of (T |^ the carrier of S) st Q[g8] holds F(g8) =
G(g8)
proof
let g1 be Element of (T |^ the carrier of S);
assume g1 in F9;
then reconsider g9 = g1 as continuous Function of S, T by Th21;
A13: g9 preserves_sup_of D & ex_sup_of D,S by WAYBEL_0:def 37,YELLOW_0:17;
the carrier of S c= dom g9 by FUNCT_2:def 1;
then
A14: the carrier of S c= dom g1;
g1.:{A(i2) where i2 is Element of S : P[i2]} = {g1.A(i) where i is
Element of S : P[i]} from FuncFraenkelS (A14);
then "\/"({g1.i where i is Element of S : i in D }, T ) = sup (g9.:D) by
Lm1
.= g1.sup D by A13;
hence thesis;
end;
{F(g3) where g3 is Element of (T |^ the carrier of S): Q[g3]} = {G(g4)
where g4 is Element of (T |^ the carrier of S): Q[g4]} from FraenkelF9RSS (A12)
;
then
A15: L = sF.sup D by Th26;
P1 is_<=_than L
proof
let b be Element of T;
assume b in P1;
then consider i9 being Element of S such that
A16: b = "\/"({g9.i9 where g9 is Element of (T |^ the carrier of S) :
g9 in F }, T ) and
A17: i9 in D;
i9 in the carrier of S;
then
A18: i9 in dom sF by FUNCT_2:def 1;
b = sF.i9 by A16,Th26;
then b in sF.:D by A17,A18,FUNCT_1:def 6;
then
A19: b <= sup (sF.:D) by YELLOW_2:22;
sF is monotone by Th29;
then sup (sF.:D) <= L by A15,WAYBEL17:15;
hence thesis by A19,YELLOW_0:def 2;
end;
then P <= L by YELLOW_0:32;
hence thesis by A11,YELLOW_0:def 3;
end;
theorem Th31:
for S, T being complete Scott TopLattice, F being non empty
Subset of ContMaps (S, T), D being directed non empty Subset of S holds "\/" ((
"\/"(F, (T |^ the carrier of S))).:D, T) = "\/" (F, (T |^ the carrier of S)).
sup D
proof
let S, T be complete Scott TopLattice, F be non empty Subset of ContMaps (S,
T), D be directed non empty Subset of S;
ContMaps (S, T) is full SubRelStr of (T |^ the carrier of S) by Def3;
then
the carrier of ContMaps (S, T) c= the carrier of (T |^ the carrier of S
) by YELLOW_0:def 13;
then reconsider F9 = F as non empty Subset of (T |^ the carrier of S) by
XBOOLE_1:1;
reconsider sF = sup F9 as Function of S, T by Th19;
set L = "\/"({ "\/"({g.i where i is Element of S : i in D }, T ) where g is
Element of (T |^ the carrier of S) : g in F }, T );
set P = "\/"({ "\/" ({g9.i9 where g9 is Element of (T |^ the carrier of S) :
g9 in F }, T ) where i9 is Element of S : i9 in D }, T);
deffunc F(Element of (T |^ the carrier of S)) = "\/"({$1.i4 where i4 is
Element of S : i4 in D }, T );
deffunc G(Element of (T |^ the carrier of S)) = $1.sup D;
defpred Q[set] means $1 in F9;
A1: for g8 being Element of (T |^ the carrier of S) st Q[g8] holds F(g8) = G
(g8)
proof
deffunc A(Element of S) = $1;
let g1 be Element of (T |^ the carrier of S);
assume g1 in F9;
then reconsider g9 = g1 as continuous Function of S, T by Th21;
defpred P[set] means $1 in D;
A2: g9 preserves_sup_of D & ex_sup_of D,S by WAYBEL_0:def 37,YELLOW_0:17;
the carrier of S c= dom g9 by FUNCT_2:def 1;
then
A3: the carrier of S c= dom g1;
g1.:{A(i2) where i2 is Element of S : P[i2]} = {g1.A(i) where i is
Element of S : P[i]} from FuncFraenkelS (A3);
then
"\/"({g1.i where i is Element of S : i in D }, T ) = sup (g9.:D) by Lm1
.= g1.sup D by A2;
hence thesis;
end;
{F(g3) where g3 is Element of (T |^ the carrier of S) : Q[g3]} = {G(g4)
where g4 is Element of (T |^ the carrier of S): Q[g4]} from FraenkelF9RSS (A1);
then
A4: L = sF.sup D by Th25;
P = sup (sF.:D) by Th27;
hence thesis by A4,Th30;
end;
theorem Th32:
for S, T being complete Scott TopLattice, F being non empty
Subset of ContMaps (S, T) holds "\/"(F, (T |^ the carrier of S)) in the carrier
of ContMaps (S, T)
proof
let S, T be complete Scott TopLattice, F be non empty Subset of ContMaps (S,
T);
reconsider Ex = "\/"(F, (T |^ the carrier of S)) as Function of S, T by Th19;
for X being Subset of S st X is non empty directed holds Ex
preserves_sup_of X
by YELLOW_0:17,Th31;
then Ex is directed-sups-preserving;
hence thesis by Def3;
end;
theorem Th33:
for S being non empty RelStr, T being lower-bounded
antisymmetric non empty RelStr holds Bottom (T |^ the carrier of S) = S -->
Bottom T
proof
let S be non empty RelStr, T be lower-bounded antisymmetric non empty RelStr;
set L = (T |^ the carrier of S);
reconsider f = S --> Bottom T as Element of L by Th19;
reconsider f9 = f as Function of S, T;
A1: for b being Element of L st b is_>=_than {} holds f <= b
proof
let b be Element of L;
reconsider b9 = b as Function of S, T by Th19;
assume b is_>=_than {};
for x being Element of S holds f9.x <= b9.x
proof
let x be Element of S;
f9. x = ((the carrier of S) --> Bottom T). x .= Bottom T by FUNCOP_1:7;
hence thesis by YELLOW_0:44;
end;
then f9 <= b9 by YELLOW_2:9;
hence thesis by WAYBEL10:11;
end;
f is_>=_than {};
then f = "\/"({}, L) by A1,YELLOW_0:30;
hence thesis by YELLOW_0:def 11;
end;
theorem
for S being non empty RelStr, T being upper-bounded antisymmetric non
empty RelStr holds Top (T |^ the carrier of S) = S --> Top T
proof
let S be non empty RelStr, T be upper-bounded antisymmetric non empty RelStr;
set L = (T |^ the carrier of S);
reconsider f = S --> Top T as Element of L by Th19;
reconsider f9 = f as Function of S, T;
A1: for b being Element of L st b is_<=_than {} holds f >= b
proof
let b be Element of L;
reconsider b9 = b as Function of S, T by Th19;
assume b is_<=_than {};
for x being Element of S holds f9.x >= b9.x
proof
let x be Element of S;
f9. x = ((the carrier of S) --> Top T). x .= Top T by FUNCOP_1:7;
hence thesis by YELLOW_0:45;
end;
then f9 >= b9 by YELLOW_2:9;
hence thesis by WAYBEL10:11;
end;
f is_<=_than {};
then f = "/\"({}, L) by A1,YELLOW_0:31;
hence thesis by YELLOW_0:def 12;
end;
registration
let S be non empty reflexive RelStr, T be complete LATTICE, a be Element of
T;
cluster S --> a -> directed-sups-preserving;
coherence
proof
set f = S --> a;
for X being Subset of S st X is non empty directed holds f
preserves_sup_of X
proof
let X be Subset of S;
assume X is non empty directed;
then reconsider X9 = X as non empty directed Subset of S;
f preserves_sup_of X
proof
assume ex_sup_of X,S;
thus ex_sup_of f.:X, T by YELLOW_0:17;
A1: {a} c= f .: X
proof
set n = the Element of X9;
let b be object;
A2: a = ((the carrier of S) --> a).n by FUNCOP_1:7
.= f.n;
assume b in {a};
then
A3: b = a by TARSKI:def 1;
dom f = the carrier of S by FUNCOP_1:13;
hence thesis by A3,A2,FUNCT_1:def 6;
end;
f .: X c= rng f by RELAT_1:111;
then f .: X c= {a} by FUNCOP_1:8;
hence sup (f.:X) = sup {a} by A1,XBOOLE_0:def 10
.= a by YELLOW_0:39
.= ((the carrier of S) --> a). sup X by FUNCOP_1:7
.= f.sup X;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th35: :: Lemma 2.4, p. 115
for S, T being complete Scott TopLattice holds ContMaps (S, T)
is sups-inheriting SubRelStr of (T |^ the carrier of S)
proof
let S, T be complete Scott TopLattice;
set L = T |^ the carrier of S;
reconsider CS = ContMaps (S, T) as full SubRelStr of L by Def3;
now
let X be Subset of CS;
assume ex_sup_of X,L;
per cases;
suppose
X is non empty;
hence "\/"(X,L) in the carrier of CS by Th32;
end;
suppose
X is empty;
then "\/"(X,L) = Bottom L by YELLOW_0:def 11;
then "\/"(X,L) = S --> Bottom T by Th33;
hence "\/"(X,L) in the carrier of CS by Def3;
end;
end;
hence thesis by YELLOW_0:def 19;
end;
registration
let S, T be complete Scott TopLattice;
cluster ContMaps (S, T) -> complete;
coherence
proof
ContMaps (S, T) is sups-inheriting non empty full SubRelStr of (T |^
the carrier of S) by Def3,Th35;
hence thesis by YELLOW_2:31;
end;
end;
theorem
for S, T being non empty Scott complete TopLattice holds Bottom
ContMaps (S, T) = S --> Bottom T
proof
let S, T be non empty Scott complete TopLattice;
set L = ContMaps (S, T);
reconsider f = S --> Bottom T as Element of L by Th21;
reconsider f9 = f as Function of S, T;
A1: for b being Element of L st b is_>=_than {} holds f <= b
proof
let b be Element of L;
reconsider b9 = b as Function of S, T by Th21;
assume b is_>=_than {};
for i being Element of S holds [f.i, b.i] in the InternalRel of T
proof
let i be Element of S;
f. i = ((the carrier of S) --> Bottom T). i .= Bottom T by FUNCOP_1:7;
then f9.i <= b9.i by YELLOW_0:44;
hence thesis;
end;
hence thesis by Th20;
end;
f is_>=_than {};
then f = "\/"({}, L) by A1,YELLOW_0:30;
hence thesis by YELLOW_0:def 11;
end;
theorem
for S, T being non empty Scott complete TopLattice holds Top ContMaps
(S, T) = S --> Top T
proof
let S, T be non empty Scott complete TopLattice;
set L = ContMaps (S, T);
reconsider f = S --> Top T as Element of L by Th21;
reconsider f9 = f as Function of S, T;
A1: for b being Element of L st b is_<=_than {} holds f >= b
proof
let b be Element of L;
reconsider b9 = b as Function of S, T by Th21;
assume b is_<=_than {};
for i being Element of S holds [b.i, f.i] in the InternalRel of T
proof
let i be Element of S;
f. i = ((the carrier of S) --> Top T). i .= Top T by FUNCOP_1:7;
then f9.i >= b9.i by YELLOW_0:45;
hence thesis;
end;
hence thesis by Th20;
end;
f is_<=_than {};
then f = "/\"({}, L) by A1,YELLOW_0:31;
hence thesis by YELLOW_0:def 12;
end;
theorem
for S, T being Scott complete TopLattice holds SCMaps (S, T) =
ContMaps (S, T)
proof
let S, T be Scott complete TopLattice;
reconsider Sm = ContMaps (S, T) as full non empty SubRelStr of (T |^ the
carrier of S) by Def3;
reconsider SC = SCMaps (S, T) as full non empty SubRelStr of (T |^ the
carrier of S) by WAYBEL15:1;
A1: the carrier of SC c= the carrier of MonMaps (S, T) by YELLOW_0:def 13;
A2: the carrier of SC c= the carrier of Sm
proof
let a be object;
assume
A3: a in the carrier of SC;
then reconsider f = a as Function of S, T by A1,WAYBEL10:9;
f is continuous Function of S, T by A3,WAYBEL17:def 2;
then a is Element of Sm by Th21;
hence thesis;
end;
the carrier of Sm c= the carrier of SC
proof
let a be object;
assume a in the carrier of Sm;
then a is continuous Function of S, T by Th21;
hence thesis by WAYBEL17:def 2;
end;
then the carrier of SC = the carrier of Sm by A2;
hence thesis by YELLOW_0:57;
end;