:: Scott-Continuous Functions
:: by Adam Grabowski
::
:: Received February 13, 1998
:: Copyright (c) 1998-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 XBOOLE_0, SUBSET_1, FUNCT_1, NUMBERS, RELAT_1, TARSKI, WAYBEL_9,
STRUCT_0, WAYBEL_0, RELAT_2, ORDERS_2, SEQM_3, XXREAL_0, WAYBEL11,
YELLOW_0, LATTICE3, ORDINAL2, PRE_TOPC, RCOMP_1, FUNCOP_1, WAYBEL_3,
REWRITE1, NEWTON, CARD_3, CAT_1, YELLOW_1, FUNCT_2, ARYTM_3, LATTICES,
WELLORD1, YELLOW_2, EQREL_1, CARD_FIL, RLVECT_3, ZFMISC_1, SETFAM_1,
YELLOW_8, TOPS_1, WAYBEL_8, WAYBEL17, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1,
FUNCT_3, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TOLER_1, ORDERS_2, LATTICE3,
YELLOW_0, ORDERS_3, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, FUNCOP_1,
WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL_2, CANTOR_1, YELLOW_8, XXREAL_0;
constructors DOMAIN_1, NAT_1, TOLER_1, ABIAN, TOPS_1, NATTRA_1, LATTICE3,
CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8, YELLOW_8, WAYBEL11,
MEMBERED, RELSET_1, TOPS_2, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
MEMBERED, ABIAN, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, YELLOW_1,
WAYBEL_2, WAYBEL_3, WAYBEL_9, WAYBEL10, WAYBEL11, PRE_TOPC, RELSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, WAYBEL_0, PRE_TOPC, RELAT_1, LATTICE3, YELLOW_0,
WAYBEL_1, WAYBEL_3, WAYBEL11, YELLOW_8, TOPS_2;
equalities WAYBEL_0, WAYBEL_3, WAYBEL11, WELLORD1, SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, WAYBEL_0, PRE_TOPC, LATTICE3, WAYBEL_1, WAYBEL_3,
WAYBEL11;
theorems WAYBEL11, WAYBEL_0, TOPS_1, TARSKI, FUNCT_1, FUNCT_2, TOPS_2,
YELLOW_0, YELLOW_2, WAYBEL_3, WAYBEL_1, RELAT_1, WAYBEL_4, ZFMISC_1,
WAYBEL_2, WAYBEL_8, NAT_1, ORDERS_2, SCHEME1, WAYBEL_9, FUNCT_3,
WAYBEL13, YELLOW_8, YELLOW_1, FUNCOP_1, WAYBEL10, RELSET_1, SETFAM_1,
XBOOLE_0, XBOOLE_1, XXREAL_0, EQREL_1;
schemes PARTFUN1, RELSET_1, FRAENKEL, XBOOLE_0;
begin :: Preliminaries
definition
let S be non empty set;
let a, b be Element of S;
func (a,b),... -> sequence of S means
:Def1:
for i being Element of NAT holds
((ex k being Element of NAT st i = 2*k) implies it.i = a) &
((not ex k being Element of NAT st i = 2*k) implies it.i = b);
existence
proof
defpred C[object] means ex k be Element of NAT st $1 = 2*k;
deffunc G(object) = b;
deffunc F(object) = a;
consider f being Function such that
A1: dom f = NAT & for x be object st x in NAT holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) from
PARTFUN1:sch 1;
A2: rng f c= {a,b}
proof
let x be object;
assume x in rng f;
then consider y be object such that
A3: y in dom f and
A4: x = f.y by FUNCT_1:def 3;
per cases;
suppose C[y];
then f.y = a by A1;
hence thesis by A4,TARSKI:def 2;
end;
suppose not C[y];
then f.y = b by A1,A3;
hence thesis by A4,TARSKI:def 2;
end;
end;
for y be object st y in {a,b} ex x be object st x in dom f & y = f.x
proof
let y be object;
assume
A5: y in {a,b};
per cases by A5,TARSKI:def 2;
suppose
A6: y = a;
take 2;
C[2]
proof
take 1;
thus thesis;
end;
hence thesis by A1,A6;
end;
suppose
A7: y = b;
take 1;
for k be Element of NAT holds 1 <> 2*k by NAT_1:15;
hence thesis by A1,A7;
end;
end;
then {a,b} c= rng f by FUNCT_1:9;
then rng f = {a,b} by A2;
then reconsider f as sequence of S by A1,FUNCT_2:def 1,RELSET_1:4;
take f;
let i be Element of NAT;
thus thesis by A1;
end;
uniqueness
proof
let f1, f2 be sequence of S;
A8: dom f1 = NAT by FUNCT_2:def 1;
A9: dom f2 = NAT by FUNCT_2:def 1;
assume that
A10: for i being Element of NAT holds
((ex k be Element of NAT st i = 2*k) implies f1.i = a) &
((not ex k be Element of NAT st i = 2*k) implies f1.i = b) and
A11: for i being Element of NAT holds
((ex k be Element of NAT st i = 2*k) implies f2.i = a) &
((not ex k be Element of NAT st i = 2*k) implies f2.i = b);
for k be object st k in NAT holds f1.k = f2.k
proof
let k be object;
assume k in NAT;
then reconsider k9 = k as Element of NAT;
per cases;
suppose
A12: ex l be Element of NAT st k = 2*l;
then f1.k = a by A10
.= f2.k by A11,A12;
hence thesis;
end;
suppose
A13: not ex l be Element of NAT st k = 2*l;
then f1.k9 = b by A10
.= f2.k9 by A11,A13;
hence thesis;
end;
end;
hence thesis by A8,A9,FUNCT_1:2;
end;
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];
A6: 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,A6,FUNCT_1:def 6;
end;
scheme FuncFraenkelSL{ B, C() -> LATTICE,
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];
A6: 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,A6,FUNCT_1:def 6;
end;
theorem Th1:
for S, T being non empty reflexive RelStr, f being Function of S, T,
P being lower Subset of T st f is monotone holds f"P is lower
proof
let S, T be non empty reflexive RelStr;
let f be Function of S, T;
let P be lower Subset of T;
assume
A1: f is monotone;
for x, y being Element of S st x in f"P & y <= x holds y in f"P
proof
let x, y be Element of S;
assume that
A2: x in f"P and
A3: y <= x;
A4: f.y <= f.x by A1,A3;
reconsider fy = f.y, fx = f.x as Element of T;
fx in P by A2,FUNCT_2:38;
then fy in P by A4,WAYBEL_0:def 19;
hence thesis by FUNCT_2:38;
end;
hence thesis;
end;
theorem
for S, T being non empty reflexive RelStr, f being Function of S, T,
P being upper Subset of T st f is monotone holds f"P is upper
proof
let S, T be non empty reflexive RelStr;
let f be Function of S, T;
let P be upper Subset of T;
assume
A1: f is monotone;
for x, y being Element of S st x in f"P & y >= x holds y in f"P
proof
let x, y be Element of S;
assume that
A2: x in f"P and
A3: y >= x;
A4: f.y >= f.x by A1,A3;
reconsider fy = f.y, fx = f.x as Element of T;
fx in P by A2,FUNCT_2:38;
then fy in P by A4,WAYBEL_0:def 20;
hence thesis by FUNCT_2:38;
end;
hence thesis;
end;
Lm1: for T being up-complete LATTICE, x being Element of T
holds downarrow x is directly_closed
proof
let T be up-complete LATTICE, x be Element of T;
let D be non empty directed Subset of T;
assume
A1: D c= downarrow x;
A2: ex_sup_of D,T by WAYBEL_0:75;
x is_>=_than D
by A1,WAYBEL_0:17;
then sup D <= x by A2,YELLOW_0:30;
hence thesis by WAYBEL_0:17;
end;
Lm2: for T being up-complete Scott TopLattice, x being Element of T
holds Cl {x} = downarrow x
proof
let T be up-complete Scott TopLattice, x be Element of T;
downarrow x is directly_closed by Lm1;
then
A1: downarrow x is closed by WAYBEL11:7;
x <= x;
then x in downarrow x by WAYBEL_0:17;
then
A2: {x} c= downarrow x by ZFMISC_1:31;
now
let C be Subset of T such that
A3: {x} c= C;
reconsider D = C as Subset of T;
assume C is closed;
then
A4: D is lower by WAYBEL11:7;
x in C by A3,ZFMISC_1:31;
hence downarrow x c= C by A4,WAYBEL11:6;
end;
hence thesis by A1,A2,YELLOW_8:8;
end;
Lm3: for T being up-complete Scott TopLattice, x being Element of T
holds downarrow x is closed
proof
let T be up-complete Scott TopLattice, x be Element of T;
Cl {x} = downarrow x by Lm2;
hence thesis;
end;
theorem Th3:
for S, T being reflexive antisymmetric non empty RelStr,
f being Function of S, T st
f is directed-sups-preserving holds f is monotone
proof
let S, T be reflexive antisymmetric non empty RelStr, f be Function of S, T;
assume
A1: f is directed-sups-preserving;
let x, y be Element of S such that
A2: x <= y;
y <= y;
then
A3: {x, y} is_<=_than y by A2,YELLOW_0:8;
A4: for
b being Element of S st {x, y} is_<=_than b holds y <= b by YELLOW_0:8;
then
A5: y = sup {x, y} by A3,YELLOW_0:30;
A6: ex_sup_of {x, y},S by A3,A4,YELLOW_0:30;
for a, b being Element of S st a in {x, y} & b in {x, y}
ex z being Element of S st z in {x, y} & a <= z & b <= z
proof
let a, b be Element of S such that
A7: a in {x, y} and
A8: b in {x, y};
take y;
thus y in {x, y} by TARSKI:def 2;
thus thesis by A2,A7,A8,TARSKI:def 2;
end;
then {x, y} is directed non empty;
then
A9: f preserves_sup_of {x, y} by A1;
then
A10: sup(f.:{x, y}) = f.y by A5,A6;
A11: dom f = the carrier of S by FUNCT_2:def 1;
then
A12: f.y = sup{f.x, f.y} by A10,FUNCT_1:60;
f.:{x, y} = {f.x, f.y} by A11,FUNCT_1:60;
then ex_sup_of {f.x, f.y}, T by A6,A9;
then {f.x, f.y} is_<=_than f.y by A12,YELLOW_0:def 9;
hence f.x <= f.y by YELLOW_0:8;
end;
registration
let S, T be reflexive antisymmetric non empty RelStr;
cluster directed-sups-preserving -> monotone for Function of S, T;
coherence by Th3;
end;
theorem Th4:
for S, T being up-complete Scott TopLattice,
f being Function of S, T holds f is continuous implies f is monotone
proof
let S, T be up-complete Scott TopLattice;
let f be Function of S, T;
assume
A1: f is continuous;
let x,y be Element of S;
A2: dom f = the carrier of S by FUNCT_2:def 1;
assume
A3: x <= y;
f.x <= f.y
proof
set V = (downarrow (f.y))`, U1 = f"V;
assume not f.x <= f.y;
then not f.x in downarrow (f.y) by WAYBEL_0:17;
then
A4: f.x in V by XBOOLE_0:def 5;
f.y <= f.y;
then
A5: f.y in downarrow (f.y) by WAYBEL_0:17;
downarrow (f.y) is closed by Lm3;
then U1 is open by A1,TOPS_2:43;
then reconsider U1 as upper Subset of S by WAYBEL11:def 4;
x in U1 by A2,A4,FUNCT_1:def 7;
then y in U1 by A3,WAYBEL_0:def 20;
then f.y in V by FUNCT_1:def 7;
hence contradiction by A5,XBOOLE_0:def 5;
end;
hence thesis;
end;
registration
let S, T be up-complete Scott TopLattice;
cluster continuous -> monotone for Function of S, T;
correctness by Th4;
end;
Lm4: for S, T being up-complete Scott non empty
reflexive transitive antisymmetric TopSpace-like TopRelStr,
f be Function of S, T holds
f is directed-sups-preserving implies f is continuous
proof
let S, T be up-complete Scott non empty reflexive transitive antisymmetric
TopSpace-like TopRelStr;
let f be Function of S, T;
assume
A1: f is directed-sups-preserving;
thus f is continuous
proof
let P1 be Subset of T;
reconsider P19 = P1 as Subset of T;
assume P1 is closed;
then
A2: P19 is directly_closed lower by WAYBEL11:7;
now
let D be non empty directed Subset of S;
assume
A3: D c= f"P1;
A4: f preserves_sup_of D by A1;
ex_sup_of D,S by WAYBEL_0:75;
then
A5: sup (f.:D) = f.sup D by A4;
reconsider fD = f.:D as directed Subset of T by A1,YELLOW_2:15;
fD c= P1 by A3,EQREL_1:46;
then sup fD in P19 by A2;
hence sup D in f"P1 by A5,FUNCT_2:38;
end;
then f"P1 is directly_closed lower by A1,A2,Th1;
hence thesis by WAYBEL11:7;
end;
end;
begin :: Poset of continuous maps
registration
let S be set;
let T be reflexive RelStr;
cluster S --> T -> reflexive-yielding;
coherence
proof
set f = S --> T;
let W be RelStr;
assume W in rng f;
hence thesis by TARSKI:def 1;
end;
end;
registration
let S be non empty set, T be complete LATTICE;
cluster T |^ S -> complete;
coherence
proof
A1: T |^ S = product (S --> T) by YELLOW_1:def 5;
for i being Element of S holds (S --> T).i is complete LATTICE;
hence thesis by A1,WAYBEL_3:31;
end;
end;
definition
let S, T be up-complete Scott TopLattice;
func SCMaps (S,T) -> strict full SubRelStr of MonMaps (S, T) means
:Def2:
for f being Function of S, T holds f in the carrier of it iff
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 MonMaps (S, T) & P[a]
from XBOOLE_0:sch 1;
X c= the carrier of MonMaps (S, T)
by A1;
then reconsider X as Subset of MonMaps (S, T);
take SX = subrelstr X;
let f be Function of S, T;
hereby
assume f in the carrier of SX;
then f in X by YELLOW_0:def 15;
then ex f9 be Function of S, T st ( f9 = f)&( f9 is continuous) by A1;
hence f is continuous;
end;
assume
A2: f is continuous;
f in Funcs (the carrier of S, the carrier of T) by FUNCT_2:8;
then f in the carrier of MonMaps (S, T) by A2,YELLOW_1:def 6;
then f in X by A1,A2;
hence thesis by YELLOW_0:def 15;
end;
uniqueness
proof
let A1, A2 be strict full SubRelStr of MonMaps (S, T);
assume that
A3: for f being Function of S,T holds f in the carrier of A1 iff
f is continuous and
A4: for f being Function of S,T holds f in the carrier of A2 iff
f is continuous;
A5: the carrier of A1 c= the carrier of MonMaps (S, T) by YELLOW_0:def 13;
A6: the carrier of A2 c= the carrier of MonMaps (S, T) by YELLOW_0:def 13;
the carrier of A1 = the carrier of A2
proof
hereby
let x be object;
assume
A7: x in the carrier of A1;
then reconsider y = x as Element of A1;
reconsider y as Function of S, T by A5,A7,WAYBEL10:9;
y is continuous by A3,A7;
hence x in the carrier of A2 by A4;
end;
let x be object;
assume
A8: x in the carrier of A2;
then reconsider y = x as Element of A2;
reconsider y as Function of S, T by A6,A8,WAYBEL10:9;
y is continuous by A4,A8;
hence thesis by A3;
end;
hence thesis by YELLOW_0:57;
end;
end;
registration
let S, T be up-complete Scott TopLattice;
cluster SCMaps (S,T) -> non empty;
coherence
proof set f = the continuous Function of S, T;
f in the carrier of SCMaps(S,T) by Def2;
hence thesis;
end;
end;
begin :: Some special nets
definition
let S be non empty RelStr;
let a, b be Element of S;
func Net-Str (a,b) -> strict non empty NetStr over S means
:Def3:
the carrier of it = NAT & the mapping of it = (a,b),... &
for i, j being Element of it, i9, j9 being Element of NAT st i = i9 & j = j9
holds i <= j iff i9 <= j9;
existence
proof
defpred P[set,set] means for i, j being Element of NAT st
i = $1 & j = $2 holds i <= j;
consider R being Relation of NAT, NAT such that
A1: for x,y being Element of NAT holds [x,y] in R iff P[x,y]
from RELSET_1:sch 2;
reconsider R as Relation of NAT;
take N = NetStr (#NAT,R,(a,b),...#);
thus the carrier of N = NAT;
thus the mapping of N = (a,b),...;
let i, j be Element of N, i9, j9 be Element of NAT such that
A2: i = i9 and
A3: j = j9;
reconsider x = i, y = j as Element of NAT;
[x,y] in the InternalRel of N iff P[x,y] by A1;
hence thesis by A2,A3,ORDERS_2:def 5;
end;
uniqueness
proof
let it1,it2 be strict non empty NetStr over S such that
A4: the carrier of it1 = NAT and
A5: the mapping of it1 = (a,b),... and
A6: for i, j being Element of it1,
i9, j9 being Element of NAT st i = i9 & j = j9
holds i <= j iff i9 <= j9 and
A7: the carrier of it2 = NAT and
A8: the mapping of it2 = (a,b),... and
A9: for i, j being Element of it2,
i9, j9 being Element of NAT st i = i9 & j = j9 holds i <= j iff i9 <= j9;
the InternalRel of it1 = the InternalRel of it2
proof
let x,y be object;
hereby
assume
A10: [x,y] in the InternalRel of it1;
then reconsider i=x, j=y as Element of it1 by ZFMISC_1:87;
reconsider i1 = i, i2 = j as Element of NAT by A4;
reconsider i9=x, j9=y as Element of it2 by A4,A7,A10,ZFMISC_1:87;
i <= j by A10,ORDERS_2:def 5;
then i1 <= i2 by A6;
then i9 <= j9 by A9;
hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5;
end;
assume
A11: [x,y] in the InternalRel of it2;
then reconsider i=x, j=y as Element of it2 by ZFMISC_1:87;
reconsider i9=x, j9=y as Element of it1 by A4,A7,A11,ZFMISC_1:87;
reconsider i1 = i, i2 = j as Element of NAT by A7;
i <= j by A11,ORDERS_2:def 5;
then i1 <= i2 by A9;
then i9 <= j9 by A6;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by A4,A5,A7,A8;
end;
end;
registration
let S be non empty RelStr;
let a, b be Element of S;
cluster Net-Str (a,b) -> reflexive transitive directed antisymmetric;
coherence
proof
set L = Net-Str (a,b);
thus L is reflexive
proof
let x be Element of L;
reconsider x9 = x as Element of NAT by Def3;
x9 <= x9;
hence thesis by Def3;
end;
thus L is transitive
proof
let x, y, z be Element of L;
assume that
A1: x <= y and
A2: y <= z;
reconsider x9 = x, y9 = y, z9 = z as Element of NAT by Def3;
A3: x9 <= y9 by A1,Def3;
y9 <= z9 by A2,Def3;
then x9 <= z9 by A3,XXREAL_0:2;
hence thesis by Def3;
end;
[#]L is directed
proof
let x, y be Element of L;
assume that x in [#]L and y in [#]L;
reconsider x9 = x, y9 = y as Element of NAT by Def3;
set z9 = x9 + y9;
reconsider z = z9 as Element of L by Def3;
reconsider z as Element of L;
take z;
A4: x9 <= z9 by NAT_1:11;
y9 <= z9 by NAT_1:11;
hence thesis by A4,Def3;
end;
hence L is directed;
thus L is antisymmetric
proof
let x, y be Element of L;
reconsider x9 = x, y9 = y as Element of NAT by Def3;
assume that
A5: x <= y and
A6: y <= x;
A7: x9 <= y9 by A5,Def3;
y9 <= x9 by A6,Def3;
hence thesis by A7,XXREAL_0:1;
end;
end;
end;
theorem Th5:
for S being non empty RelStr, a, b being Element of S,
i being Element of Net-Str (a, b) holds
Net-Str (a, b).i = a or Net-Str (a, b).i = b
proof
let S be non empty RelStr;
let a, b be Element of S, i be Element of Net-Str (a, b);
set N = Net-Str (a,b);
reconsider I = i as Element of NAT by Def3;
A1: N.i = (a,b),....i by Def3;
defpred C[Element of NAT] means ex k be Element of NAT st $1 = 2*k;
per cases;
suppose C[I];
hence thesis by A1,Def1;
end;
suppose not C[I];
hence thesis by A1,Def1;
end;
end;
theorem Th6:
for S being non empty RelStr, a, b being Element of S,
i, j being Element of Net-Str (a,b),
i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
(Net-Str (a, b).i = a implies Net-Str (a, b).j = b) &
(Net-Str (a, b).i = b implies Net-Str (a, b).j = a)
proof
let S be non empty RelStr;
let a, b be Element of S,
i, j be Element of Net-Str (a,b), i9, j9 be Element of NAT;
assume that
A1: i9 = i and
A2: j9 = i9 + 1 and
A3: j9 = j;
per cases;
suppose
A4: a <> b;
defpred C[Element of NAT] means ex k be Element of NAT st $1 = 2*k;
thus Net-Str (a, b).i = a implies Net-Str (a, b).j = b
proof
assume
A5: Net-Str (a, b).i = a;
C[i9]
proof
assume
A6: not C[i9];
Net-Str (a, b).i = (a,b),....i by Def3
.= b by A1,A6,Def1;
hence thesis by A4,A5;
end;
then
A7: for k be Element of NAT holds j9 <> 2*k by A2;
Net-Str (a, b).j = (a,b),....j by Def3
.= b by A3,A7,Def1;
hence thesis;
end;
assume
A8: Net-Str (a, b).i = b;
A9: not C[i9]
proof
assume
A10: C[i9];
Net-Str (a, b).i = (a,b),....i by Def3
.= a by A1,A10,Def1;
hence thesis by A4,A8;
end;
A11: C[j9]
proof
assume not C[j9];
then ex kl be Element of NAT st ( j9 = 2*kl + 1) by SCHEME1:1;
hence thesis by A2,A9;
end;
Net-Str (a, b).j = (a,b),....j by Def3
.= a by A3,A11,Def1;
hence thesis;
end;
suppose a = b;
hence thesis by Th5;
end;
end;
theorem Th7:
for S being with_infima Poset, a, b being Element of S holds
lim_inf Net-Str (a,b) = a "/\" b
proof
let S be with_infima Poset;
let a, b be Element of S;
set N = Net-Str (a,b);
A1: for
j be Element of N holds {N.i where i is Element of N : i >= j} = {a,b}
proof
let j be Element of N;
thus {N.i where i is Element of N : i >= j} c= {a,b}
proof
let x be object;
assume x in {N.i where i is Element of N : i >= j};
then consider i1 be Element of N such that
A2: x = N.i1 and i1 >= j;
N.i1 = a or N.i1 = b by Th5;
hence thesis by A2,TARSKI:def 2;
end;
thus {a,b} c= {N.i where i is Element of N : i >= j}
proof
let x be object;
assume
A3: x in {a,b};
reconsider J = j as Element of NAT by Def3;
defpred C[Element of NAT] means ex k be Element of NAT st $1 = 2*k;
per cases by A3,TARSKI:def 2;
suppose
A4: x = a;
now per cases;
suppose
A5: C[J];
A6: N.j = (a,b),....j by Def3
.= a by A5,Def1;
j <= j;
hence thesis by A4,A6;
end;
suppose
A7: not C[J];
A8: N.j = (a,b),....j by Def3
.= b by A7,Def1;
reconsider k = J + 1 as Element of N by Def3;
A9: N.k = a by A8,Th6;
J + 1 >= J by NAT_1:11;
then k >= j by Def3;
hence thesis by A4,A9;
end;
end;
hence thesis;
end;
suppose
A10: x = b;
now per cases;
suppose
A11: not C[J];
A12: N.j = (a,b),....j by Def3
.= b by A11,Def1;
j <= j;
hence thesis by A10,A12;
end;
suppose
A13: C[J];
A14: N.j = (a,b),....j by Def3
.= a by A13,Def1;
reconsider k = J + 1 as Element of N by Def3;
A15: N.k = b by A14,Th6;
J + 1 >= J by NAT_1:11;
then k >= j by Def3;
hence thesis by A10,A15;
end;
end;
hence thesis;
end;
end;
end;
defpred P[Element of N,Element of N] means $1 >= $2;
deffunc F(Element of N) = {N.i1 where i1 is Element of N : P[i1,$1]};
defpred R[set] means not contradiction;
deffunc G(Element of N) = {a, b};
deffunc Q1(Element of N) = "/\"(F($1), S);
deffunc Q2(Element of N) = "/\"(G($1), S);
deffunc F(set) = a "/\" b;
A16: for jj be Element of N holds Q1(jj) = F(jj)
proof
let jj be Element of N;
Q1(jj) = Q2(jj) by A1
.= a "/\" b by YELLOW_0:40;
hence thesis;
end;
A17: {Q1(j3) where j3 is Element of N : R[j3]} =
{F(j4) where j4 is Element of N : R[j4]} from FRAENKEL:sch 5(A16);
A18: {a "/\" b where j4 is Element of N : R[j4]} c= {a "/\" b}
proof
let x be object;
assume x in {a "/\" b where j4 is Element of N : R[j4]};
then ex q be Element of N st ( x = a "/\" b)&( R[q]);
hence thesis by TARSKI:def 1;
end;
{a "/\" b} c= {a "/\" b where j4 is Element of N : R[j4]}
proof
let x be object;
assume x in {a "/\" b};
then x = a "/\" b by TARSKI:def 1;
hence thesis;
end;
then {a "/\" b where j4 is Element of N : R[j4]} = {a "/\" b} by A18;
hence thesis by A17,YELLOW_0:39;
end;
Lm5: for S being with_infima Poset, a, b being Element of S st a <= b holds
lim_inf Net-Str (a,b) = a
proof
let S be with_infima Poset;
let a, b be Element of S such that
A1: a <= b;
reconsider a9 = a, b9 = b as Element of S;
lim_inf Net-Str (a,b) = a9 "/\" b9 by Th7
.= a9 by A1,YELLOW_0:25;
hence thesis;
end;
theorem Th8:
for S, T being with_infima Poset, a, b being Element of S,
f being Function of S, T holds lim_inf (f*Net-Str (a,b)) = f.a "/\" f.b
proof
let S, T be with_infima Poset;
let a, b be Element of S;
let f be Function of S, T;
set N = Net-Str (a,b);
set fN = f * N;
A1: the RelStr of fN = the RelStr of N by WAYBEL_9:def 8;
A2: for j being Element of fN holds
{fN.i where i is Element of fN : i >= j} = {f.a, f.b}
proof
let j be Element of fN;
reconsider jj = j as Element of N by A1;
thus {fN.i where i is Element of fN : i >= j} c= {f.a,f.b}
proof
let x be object;
assume x in {fN.i where i is Element of fN : i >= j};
then consider i1 be Element of fN such that
A3: x = fN.i1 and i1 >= j;
reconsider I1 = i1 as Element of N by A1;
i1 in the carrier of N by A1;
then
A4: i1 in dom the mapping of N by FUNCT_2:def 1;
fN.i1 = (f * the mapping of N).i1 by WAYBEL_9:def 8
.= f.(N.I1) by A4,FUNCT_1:13;
then fN.i1 = f.a or fN.i1 = f.b by Th5;
hence thesis by A3,TARSKI:def 2;
end;
thus {f.a,f.b} c= {fN.i where i is Element of fN : i >= j}
proof
let x be object;
assume
A5: x in {f.a,f.b};
A6: j in the carrier of N by A1;
reconsider J = j as Element of NAT by A1,Def3;
A7: j in dom the mapping of N by A6,FUNCT_2:def 1;
defpred C[Element of NAT] means ex k be Element of NAT st $1 = 2*k;
per cases by A5,TARSKI:def 2;
suppose
A8: x = f.a;
reconsider jj = j as Element of N by A1;
now per cases;
suppose
A9: C[J];
A10: fN.j = (f * the mapping of N).j by WAYBEL_9:def 8
.= f.((the mapping of N).j) by A7,FUNCT_1:13
.= f.((a,b),....j) by Def3
.= f.a by A9,Def1;
j <= j;
hence thesis by A8,A10;
end;
suppose
A11: not C[J];
A12: N.jj = (a,b),....jj by Def3
.= b by A11,Def1;
reconsider k = J + 1 as Element of fN by A1,Def3;
reconsider kk = k as Element of N by A1;
kk in the carrier of N;
then
A13: kk in dom the mapping of N by FUNCT_2:def 1;
A14: fN.k = (f * the mapping of N).k by WAYBEL_9:def 8
.= f.(N.kk) by A13,FUNCT_1:13
.= f.a by A12,Th6;
J + 1 >= J by NAT_1:11;
then kk >= jj by Def3;
then [jj,kk] in the InternalRel of N by ORDERS_2:def 5;
then k >= j by A1,ORDERS_2:def 5;
hence thesis by A8,A14;
end;
end;
hence thesis;
end;
suppose
A15: x = f.b;
now per cases;
suppose
A16: not C[J];
A17: fN.j = (f * the mapping of N).j by WAYBEL_9:def 8
.= f.((the mapping of N).j) by A7,FUNCT_1:13
.= f.((a,b),....j) by Def3
.= f.b by A16,Def1;
j <= j;
hence thesis by A15,A17;
end;
suppose
A18: C[J];
A19: N.jj = (a,b),....j by Def3
.= a by A18,Def1;
reconsider k = J + 1 as Element of fN by A1,Def3;
reconsider kk = k as Element of N by Def3;
kk in the carrier of N;
then
A20: kk in dom the mapping of N by FUNCT_2:def 1;
A21: fN.k = (f * the mapping of N).k by WAYBEL_9:def 8
.= f.(N.kk) by A20,FUNCT_1:13
.= f.b by A19,Th6;
J + 1 >= J by NAT_1:11;
then kk >= jj by Def3;
then [jj,kk] in the InternalRel of N by ORDERS_2:def 5;
then k >= j by A1,ORDERS_2:def 5;
hence thesis by A15,A21;
end;
end;
hence thesis;
end;
end;
end;
defpred P[Element of fN,Element of fN] means $1 >= $2;
deffunc F(Element of fN) = {fN.i1 where i1 is Element of fN : P[i1,$1]};
defpred R[set] means not contradiction;
deffunc G(Element of fN) = {f.a, f.b};
deffunc Q1(Element of fN) = "/\"(F($1), T);
deffunc Q2(Element of fN) = "/\"(G($1), T);
deffunc F(set) = f.a "/\" f.b;
A22: for jj be Element of fN holds Q1(jj) = F(jj)
proof
let jj be Element of fN;
Q1(jj) = Q2(jj) by A2
.= f.a "/\" f.b by YELLOW_0:40;
hence thesis;
end;
A23: {Q1(j3) where j3 is Element of fN : R[j3]} =
{F(j4) where j4 is Element of fN : R[j4]} from FRAENKEL:sch 5(A22);
A24: {f.a "/\" f.b where j4 is Element of fN : R[j4]} c= {f.a "/\" f.b}
proof
let x be object;
assume x in {f.a "/\" f.b where j4 is Element of fN : R[j4]};
then ex q be Element of fN st ( x = f.a "/\" f.b)&( R[q]);
hence thesis by TARSKI:def 1;
end;
{f.a "/\" f.b} c= {f.a "/\" f.b where j4 is Element of fN : R[j4]}
proof
let x be object;
assume x in {f.a "/\" f.b};
then x = f.a "/\" f.b by TARSKI:def 1;
hence thesis;
end;
then {f.a "/\" f.b where j4 is Element of fN : R[j4]} = {f.a "/\" f.b} by A24
;
hence thesis by A23,YELLOW_0:39;
end;
definition
let S be non empty RelStr;
let D be non empty Subset of S;
func Net-Str D -> strict NetStr over S equals
NetStr (#D, (the InternalRel of S)|_2 D, (id the carrier of S)|D#);
correctness;
end;
theorem Th9:
for S being non empty reflexive RelStr, D being non empty Subset of S holds
Net-Str D = Net-Str (D, (id the carrier of S)|D)
proof
let S be non empty reflexive RelStr;
let D be non empty Subset of S;
set M = Net-Str (D, (id the carrier of S)|D);
A1: D = the carrier of M by WAYBEL11:def 10;
A2: (id the carrier of S)|D = the mapping of M by WAYBEL11:def 10;
A3: (id the carrier of S)|D = id D by FUNCT_3:1;
A4: (the InternalRel of S)|_2 D c= the InternalRel of S by XBOOLE_1:17;
now
let x, y be object;
hereby
assume
A5: [x,y] in (the InternalRel of S)|_2 D;
then
A6: x in D by ZFMISC_1:87;
A7: y in D by A5,ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of M by A1,A5,ZFMISC_1:87;
A8: x9 = ((id the carrier of S)|D).x9 by A3,A6,FUNCT_1:18;
y9 = ((id the carrier of S)|D).y9 by A3,A7,FUNCT_1:18;
then M.x9 <= M.y9 by A2,A4,A5,A8,ORDERS_2:def 5;
then x9 <= y9 by WAYBEL11:def 10;
hence [x,y] in the InternalRel of M by ORDERS_2:def 5;
end;
assume
A9: [x,y] in the InternalRel of M;
then reconsider x9 = x, y9 = y as Element of M by ZFMISC_1:87;
x9 <= y9 by A9,ORDERS_2:def 5;
then M.x9 <= M.y9 by WAYBEL11:def 10;
then
A10: [M.x9, M.y9] in the InternalRel of S by ORDERS_2:def 5;
A11: x9 = ((id the carrier of S)|D).x9 by A1,A3;
y9 = ((id the carrier of S)|D). y9 by A1,A3;
hence [x,y] in (the InternalRel of S)|_2 D by A1,A2,A9,A10,A11,
XBOOLE_0:def 4;
end;
hence thesis by A1,A2,RELAT_1:def 2;
end;
registration
let S be non empty reflexive RelStr;
let D be directed non empty Subset of S;
cluster Net-Str D -> non empty directed reflexive;
coherence
proof
Net-Str D = Net-Str (D, (id the carrier of S)|D) by Th9;
hence thesis;
end;
end;
registration
let S be non empty reflexive transitive RelStr;
let D be directed non empty Subset of S;
cluster Net-Str D -> transitive;
coherence;
end;
registration
let S be non empty reflexive RelStr;
let D be directed non empty Subset of S;
cluster Net-Str D -> monotone;
coherence
proof
Net-Str D = Net-Str (D, (id the carrier of S)|D) by Th9;
hence thesis;
end;
end;
Lm6: for R being up-complete LATTICE, N being monotone reflexive net of R
holds lim_inf N = sup N
proof
let R be up-complete LATTICE, N be monotone reflexive net of R;
defpred P[set] means not contradiction;
deffunc F(Element of N) = N.$1;
deffunc G(Element of N) = "/\"({N.i where i is Element of N: i >= $1}, R);
A1: for j being Element of N holds F(j) = G(j)
proof
let j be Element of N;
set Y = {N.i where i is Element of N: i >= j};
A2: N.j is_<=_than Y
proof
let y be Element of R;
assume y in Y;
then ex i being Element of N st y = N.i & j <= i;
hence N.j <= y by WAYBEL11:def 9;
end;
for b being Element of R st b is_<=_than Y holds N.j >= b
proof
let b be Element of R;
assume
A3: b is_<=_than Y;
reconsider j9 = j as Element of N;
j9 <= j9;
then N.j9 in Y;
hence thesis by A3;
end;
hence thesis by A2,YELLOW_0:31;
end;
rng the mapping of N = { F(j) where j is Element of N: P[j]} by WAYBEL11:19
.= {G(j) where j is Element of N: P[j]} from FRAENKEL:sch 5(A1);
hence lim_inf N = Sup the mapping of N by YELLOW_2:def 5
.= sup N by WAYBEL_2:def 1;
end;
theorem Th10:
for S being up-complete LATTICE,
D being directed non empty Subset of S holds lim_inf Net-Str D = sup D
proof
let S be up-complete LATTICE;
let D be directed non empty Subset of S;
set F = (id the carrier of S)|D;
A1: F = id D by FUNCT_3:1;
lim_inf Net-Str D = sup Net-Str D by Lm6
.= Sup F by WAYBEL_2:def 1
.= "\/"(rng F, S) by YELLOW_2:def 5
.= sup D by A1,RELAT_1:45;
hence thesis;
end;
begin :: Monotone maps
theorem Th11:
for S, T being LATTICE, f being Function of S, T holds
(for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)) implies
f is monotone
proof
let S, T be LATTICE;
let f be Function of S, T;
assume
A1: for N be net of S holds f.(lim_inf N) <= lim_inf (f*N);
now
let a, b be Element of S;
assume
A2: a <= b;
set N = Net-Str (a,b);
A3: f.(lim_inf N) = f.a by A2,Lm5;
lim_inf (f*N) = f.a "/\" f.b by Th8;
then
A4: f.a <= f.a "/\" f.b by A1,A3;
f.a >= f.a "/\" f.b by YELLOW_0:23;
then f.a = f.a "/\" f.b by A4,ORDERS_2:2;
hence f.a <= f.b by YELLOW_0:25;
end;
hence thesis;
end;
scheme NetFraenkelS{B, B1, 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 B1(): P[x]}
provided
A1: the carrier of C() c= dom f() and
A2: the carrier of B() = the carrier of B1()
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 B1(): 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
A3: z in {A(x) where x is Element of B(): P[x]} and
A4: y = f.z by FUNCT_1:def 6;
consider x being Element of B() such that
A5: z = A(x) and
A6: P[x] by A3;
reconsider x as Element of B1() by A2;
y = f.A(x) by A4,A5;
hence thesis by A6;
end;
let y be object;
assume y in {f.A(x) where x is Element of B1(): P[x]};
then consider x being Element of B1() such that
A7: y = f.A(x) and
A8: P[x];
reconsider x as Element of B() by A2;
A9: A(x) in the carrier of C();
A(x) in {A(z) where z is Element of B(): P[z]} by A8;
hence thesis by A1,A7,A9,FUNCT_1:def 6;
end;
theorem Th12:
for S, T being continuous lower-bounded LATTICE,
f being Function of S, T holds ( f is directed-sups-preserving implies
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 continuous lower-bounded LATTICE;
let f be Function of S, T;
assume
A1: f is directed-sups-preserving;
let x be Element of S;
defpred P[Element of S] means $1 << x;
deffunc A(Element of S) = $1;
A2: f preserves_sup_of waybelow x by A1;
A3: ex_sup_of waybelow x,S by YELLOW_0:17;
A4: the carrier of S c= dom f by FUNCT_2:def 1;
A5: f.:{ A(w) where w is Element of S : P[w] } =
{f.A(w) where w is Element of S : P[w] } from FuncFraenkelSL(A4);
f.x = f.(sup waybelow x) by WAYBEL_3:def 5
.= "\/"({f.w where w is Element of S : w << x },T) by A2,A3,A5;
hence thesis;
end;
theorem Th13:
for S being LATTICE, T being up-complete lower-bounded LATTICE,
f being 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) ) implies
f is monotone)
proof
let S be LATTICE, T be up-complete lower-bounded LATTICE;
let f be Function of S, T;
assume
A1: for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T);
let X,Y be Element of S;
deffunc A(Element of S) = $1;
defpred P[Element of S] means $1 << X;
defpred Q[Element of S] means $1 << Y;
assume X <= Y;
then
A2: waybelow X c= waybelow Y by WAYBEL_3:12;
A3: f.X = "\/"({ f.w where w is Element of S : w << X },T) by A1;
A4: the carrier of S c= dom f by FUNCT_2:def 1;
A5: f.:{ A(w) where w is Element of S : P[w] } =
{ f.A(w) where w is Element of S : P[w] } from FuncFraenkelSL(A4);
f.:{ A(w) where w is Element of S : Q[w] } =
{ f.A(w) where w is Element of S : Q[w] } from FuncFraenkelSL(A4);
then
A6: f.Y = "\/"(f.:waybelow Y,T) by A1;
A7: ex_sup_of f.:waybelow X,T by YELLOW_0:17;
ex_sup_of f.:waybelow Y,T by YELLOW_0:17;
hence thesis by A2,A3,A5,A6,A7,RELAT_1:123,YELLOW_0:34;
end;
theorem Th14:
for S being up-complete lower-bounded LATTICE,
T being continuous lower-bounded LATTICE, f being 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) ) implies
for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w )
proof
let S be up-complete lower-bounded LATTICE;
let T be continuous lower-bounded LATTICE;
let f be Function of S, T;
assume
A1: for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T);
then
A2: f is monotone by Th13;
let x be Element of S, y be Element of T;
hereby
assume
A3: y << f.x;
reconsider D = f.:(waybelow x) as non empty directed Subset of T
by A1,Th13,YELLOW_2:15;
A4: f.x = "\/"({ f.w where w is Element of S : w << x },T) by A1;
A5: the carrier of S c= dom f by FUNCT_2:def 1;
defpred P[Element of S] means $1 << x;
deffunc A(Element of S) = $1;
f.:{ A(w) where w is Element of S : P[w] } =
{ f.A(w) where w is Element of S : P[w] } from FuncFraenkelSL(A5);
then consider w being Element of T such that
A6: w in D and
A7: y << w by A3,A4,WAYBEL_4:53;
consider v be object such that
A8: v in the carrier of S and
A9: v in waybelow x and
A10: w = f.v by A6,FUNCT_2:64;
reconsider v as Element of S by A8;
take v;
thus v << x & y << f.v by A7,A9,A10,WAYBEL_3:7;
end;
given w being Element of S such that
A11: w << x and
A12: y << f.w;
w <= x by A11,WAYBEL_3:1;
then f.w <= f.x by A2;
hence thesis by A12,WAYBEL_3:2;
end;
theorem Th15:
for S, T being non empty RelStr, D being Subset of S,
f being Function of S, T st ex_sup_of D,S & ex_sup_of f.:D,T or
S is complete antisymmetric & T is complete antisymmetric holds
f is monotone implies sup (f.:D) <= f.(sup D)
proof
let S, T be non empty RelStr;
let D be Subset of S;
let f be Function of S, T;
assume that
A1: ex_sup_of D,S & ex_sup_of f.:D,T or
S is complete antisymmetric & T is complete antisymmetric;
A2: ex_sup_of D,S by A1,YELLOW_0:17;
A3: ex_sup_of f.:D,T by A1,YELLOW_0:17;
assume
A4: f is monotone;
D is_<=_than sup D by A2,YELLOW_0:def 9;
then f.:D is_<=_than f.(sup D) by A4,YELLOW_2:14;
hence thesis by A3,YELLOW_0:def 9;
end;
theorem Th16:
for S, T being non empty reflexive antisymmetric RelStr,
D being directed non empty Subset of S, f being Function of S, T st
ex_sup_of D,S & ex_sup_of f.:D,T or
S is up-complete & T is up-complete holds
f is monotone implies sup (f.:D) <= f.(sup D)
proof
let S, T be non empty reflexive antisymmetric RelStr;
let D be directed non empty Subset of S;
let f be Function of S, T;
assume that
A1: ex_sup_of D,S & ex_sup_of f.:D,T or S is up-complete & T is up-complete;
assume
A2: f is monotone;
then reconsider fD = f.:D as directed non empty Subset of T by YELLOW_2:15;
A3: ex_sup_of fD, T by A1,WAYBEL_0:75;
ex_sup_of D, S by A1,WAYBEL_0:75;
then D is_<=_than sup D by YELLOW_0:30;
then f.:D is_<=_than f.(sup D) by A2,YELLOW_2:14;
hence thesis by A3,YELLOW_0:30;
end;
theorem
for S, T being non empty RelStr, D being Subset of S,
f being Function of S, T st ex_inf_of D,S & ex_inf_of f.:D,T or
S is complete antisymmetric & T is complete antisymmetric holds
f is monotone implies f.(inf D) <= inf (f.:D)
proof
let S, T be non empty RelStr;
let D be Subset of S;
let f be Function of S, T;
assume that
A1: ex_inf_of D,S & ex_inf_of f.:D,T or
S is complete antisymmetric & T is complete antisymmetric;
A2: ex_inf_of D,S by A1,YELLOW_0:17;
A3: ex_inf_of f.:D,T by A1,YELLOW_0:17;
assume
A4: f is monotone;
inf D is_<=_than D by A2,YELLOW_0:def 10;
then f.(inf D) is_<=_than f.:D by A4,YELLOW_2:13;
hence thesis by A3,YELLOW_0:def 10;
end;
Lm7: for S, T being complete LATTICE, D being Subset of S,
f being Function of S, T holds
f is monotone implies f.("/\"(D,S)) <= inf (f.:D)
proof
let S, T be complete LATTICE;
let D be Subset of S;
let f be Function of S, T;
reconsider D9 = D as Subset of S;
set infD = "/\"(D,S);
assume
A1: f is monotone;
infD is_<=_than D by YELLOW_0:33;
then f.(infD) is_<=_than f.:D9 by A1,YELLOW_2:13;
hence thesis by YELLOW_0:33;
end;
theorem Th18:
for S, T being up-complete LATTICE, f being Function of S, T,
N being monotone non empty NetStr over S holds
f is monotone implies f * N is monotone
proof
let S, T be up-complete LATTICE, f be Function of S, T;
let N be monotone non empty NetStr over S;
assume
A1: f is monotone;
A2: netmap (N, S) is monotone by WAYBEL_0:def 9;
A3: netmap (f * N, T) = f * netmap (N, S) by WAYBEL_9:def 8;
set g = netmap (f * N, T);
now
let x, y be Element of f * N;
assume
A4: x <= y;
A5: the RelStr of N = the RelStr of (f * N) by WAYBEL_9:def 8;
then reconsider x9 = x, y9 = y as Element of N;
A6: dom netmap (N, S) = the carrier of (f * N) by A5,FUNCT_2:def 1;
then
A7: netmap (f * N, T).x = f.(netmap (N, S).x) by A3,FUNCT_1:13;
A8: netmap (f * N, T).y = f.(netmap (N, S).y) by A3,A6,FUNCT_1:13;
[x,y] in the InternalRel of (f * N) by A4,ORDERS_2:def 5;
then x9 <= y9 by A5,ORDERS_2:def 5;
then netmap (N, S).x9 <= netmap (N, S).y9 by A2;
hence g.x <= g.y by A1,A7,A8;
end;
then netmap (f * N, T) is monotone;
hence thesis;
end;
registration
let S, T be up-complete LATTICE;
let f be monotone Function of S, T;
let N be monotone non empty NetStr over S;
cluster f * N -> monotone;
coherence by Th18;
end;
theorem
for S, T being up-complete LATTICE, f being Function of S, T holds
(for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)) implies
for D being directed non empty Subset of S holds sup (f.:D) = f.(sup D)
proof
let S, T be up-complete LATTICE, f be Function of S, T;
assume
A1: for N being net of S holds f.(lim_inf N) <= lim_inf (f*N);
let D be directed non empty Subset of S;
A2: f is monotone by A1,Th11;
then
A3: sup (f.:D) <= f.(sup D) by Th16;
f.(sup D) <= sup (f.:D)
proof
sup D = lim_inf Net-Str D by Th10;
then
A4: f.(sup D) <= lim_inf (f*(Net-Str D)) by A1;
reconsider fN = f*(Net-Str D) as monotone reflexive net of T by A2;
A5: sup fN = Sup the mapping of fN by WAYBEL_2:def 1
.= Sup (f * (id the carrier of S)|D) by WAYBEL_9:def 8
.= sup (rng (f * (id the carrier of S)|D)) by YELLOW_2:def 5;
rng (f * (id the carrier of S)|D) = rng (f * id D) by FUNCT_3:1
.= rng (f|D) by RELAT_1:65
.= f .: D by RELAT_1:115;
hence thesis by A4,A5,Lm6;
end;
hence thesis by A3,ORDERS_2:2;
end;
Lm8: for S, T being complete LATTICE, f being Function of S, T holds
(for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)) implies
f is directed-sups-preserving
proof
let S, T be complete LATTICE, f be Function of S, T;
assume
A1: for N being net of S holds f.(lim_inf N) <= lim_inf (f*N);
thus f is directed-sups-preserving
proof
let D be Subset of S;
assume D is non empty directed;
then reconsider D as non empty directed Subset of S;
A2: f is monotone by A1,Th11;
then
A3: sup (f.:D) <= f.(sup D) by Th15;
A4: f.(sup D) <= sup (f.:D)
proof
sup D = lim_inf Net-Str D by Th10;
then
A5: f.(sup D) <= lim_inf (f*(Net-Str D)) by A1;
reconsider fN = f*(Net-Str D) as monotone reflexive net of T by A2;
A6: sup fN = Sup the mapping of fN by WAYBEL_2:def 1
.= Sup (f * (id the carrier of S)|D) by WAYBEL_9:def 8
.= sup (rng (f * (id the carrier of S)|D)) by YELLOW_2:def 5;
rng (f * (id the carrier of S)|D) = rng (f * id D) by FUNCT_3:1
.= rng (f|D) by RELAT_1:65
.= f .: D by RELAT_1:115;
hence thesis by A5,A6,WAYBEL11:22;
end;
f preserves_sup_of D
by A3,A4,ORDERS_2:2,YELLOW_0:17;
hence thesis;
end;
end;
theorem Th20:
for S, T being complete LATTICE, f being Function of S, T, N being net of S,
j being Element of N, j9 being Element of (f*N) st j9 = j
holds f is monotone implies f."/\"({N.k where k is Element of N: k >= j},S)
<= "/\"({(f*N).l where l is Element of (f*N) : l >= j9},T)
proof
let S, T be complete LATTICE, f be Function of S, T;
let N be net of S;
let j be Element of N, j9 be Element of (f*N);
assume
A1: j9 = j;
assume
A2: f is monotone;
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: the RelStr of (f*N) = the RelStr of N by WAYBEL_9:def 8;
A5: dom (the mapping of N) = the carrier of N by FUNCT_2:def 1;
A6: {(f*N).l where l is Element of (f*N) : l >= j9} c=
f.:{N.l1 where l1 is Element of N : l1 >= j}
proof
let s be object;
assume s in {(f*N).l where l is Element of (f*N) : l >= j9};
then consider x being Element of (f*N) such that
A7: s = (f*N).x and
A8: x >= j9;
reconsider x as Element of N by A4;
[j9,x] in the InternalRel of (f*N) by A8,ORDERS_2:def 5;
then
A9: x >= j by A1,A4,ORDERS_2:def 5;
A10: s = (f*the mapping of N).x by A7,WAYBEL_9:def 8
.= f.(N.x) by A5,FUNCT_1:13;
N.x in {N.z where z is Element of N : z >= j} by A9;
hence thesis by A3,A10,FUNCT_1:def 6;
end;
A11: f.:{N.l1 where l1 is Element of N : l1 >= j} c=
{(f*N).l where l is Element of (f*N) : l >= j9}
proof
let s be object;
assume s in f.:{N.l1 where l1 is Element of N : l1 >= j};
then consider x be object such that
x in dom f and
A12: x in {N.l1 where l1 is Element of N : l1 >= j} and
A13: s = f.x by FUNCT_1:def 6;
consider l2 being Element of N such that
A14: x = N.l2 and
A15: l2 >= j by A12;
reconsider l29 = l2 as Element of (f*N) by A4;
A16: s = (f*the mapping of N).l2 by A5,A13,A14,FUNCT_1:13
.= (f*N).l29 by WAYBEL_9:def 8;
[j, l2] in the InternalRel of N by A15,ORDERS_2:def 5;
then l29 >= j9 by A1,A4,ORDERS_2:def 5;
hence thesis by A16;
end;
set K = {N.k where k is Element of N: k >= j};
K c= the carrier of S
proof
let r be object;
assume r in K;
then ex f being Element of N st ( r = N.f)&( f >= j);
hence thesis;
end;
then reconsider K as Subset of S;
{(f*N).l where l is Element of (f*N) : l >= j9} = f.:K by A6,A11;
hence thesis by A2,Lm7;
end;
Lm9: for S, T being complete Scott TopLattice,
f being continuous Function of S, T holds
for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)
proof
let S, T be complete Scott TopLattice, f be continuous Function of S, T;
let N be net of S;
set x = lim_inf N;
set t = lim_inf (f * N);
assume not f.x <= t;
then not f.x in downarrow t by WAYBEL_0:17;
then
A1: f.x in (downarrow t)` by XBOOLE_0:def 5;
A2: downarrow t is closed by Lm3;
set U1 = f"((downarrow t)`);
A3: U1 is open by A2,TOPS_2:43;
set D = the set of all "/\"({N.k where k is Element of N: k >= j},S)
where j is Element of N;
now
let f be object;
assume f in D;
then ex j be Element of N st ( f = "/\"({N.k where k is Element
of N: k >= j},S));
hence f in the carrier of S;
end;
then reconsider D as Subset of S by TARSKI:def 3;
reconsider D as non empty directed Subset of S by WAYBEL11:30;
A4: x in U1 by A1,FUNCT_2:38;
U1 is property(S) by A3,WAYBEL11:15;
then consider y being Element of S such that
A5: y in D and
A6: for x being Element of S st x in D & x >= y holds x in U1
by A4;
consider j be Element of N such that
A7: y = "/\"({N.k where k is Element of N: k >= j},S) by A5;
y <= y;
then
A8: y in U1 by A5,A6;
the RelStr of (f * N) = the RelStr of N by WAYBEL_9:def 8;
then reconsider j9 = j as Element of (f * N);
A9: dom f = the carrier of S by FUNCT_2:def 1;
set fy = "/\" ({(f*N).k where k is Element of (f*N) : k >= j9},T);
set fD = the set of all "/\"({(f*N).k where k is Element of (f*N) : k >=
j1},T) where j1 is Element of (f*N) ;
now
let g be object;
assume g in fD;
then ex j be Element of (f*N) st ( g = "/\" ({(f*N).k where k is
Element of (f*N) : k >= j},T));
hence g in the carrier of T;
end;
then reconsider fD as Subset of T by TARSKI:def 3;
A10: f.y <= fy by A7,Th20;
fy in fD;
then fy <= sup fD by YELLOW_2:22;
then f.y <= t by A10,ORDERS_2:3;
then f.y in downarrow t by WAYBEL_0:17;
then
A11: y in f"(downarrow t) by A9,FUNCT_1:def 7;
f"((downarrow t)`) = f"([#]T) \ f"(downarrow t) by FUNCT_1:69
.= [#]S \ f"(downarrow t) by TOPS_2:41
.= (f"(downarrow t))`;
then
A12: y in U1 /\ U1` by A8,A11,XBOOLE_0:def 4;
U1 misses U1` by XBOOLE_1:79;
hence contradiction by A12;
end;
Lm10: for L being continuous Scott TopLattice,
p be Element of L, S be Subset of L st S is open & p in S
ex q being Element of L st q << p & q in S
proof
let L be continuous Scott TopLattice, p be Element of L;
let S be Subset of L such that
A1: S is open and
A2: p in S;
A3: S is inaccessible by A1,WAYBEL11:def 4;
sup waybelow p = p by WAYBEL_3:def 5;
then waybelow p meets S by A2,A3;
then (waybelow p) /\ S <> {};
then consider u being object such that
A4: u in (waybelow p) /\ S by XBOOLE_0:def 1;
A5: u in waybelow p by A4,XBOOLE_0:def 4;
reconsider u as Element of L by A4;
take u;
thus u << p by A5,WAYBEL_3:7;
thus thesis by A4,XBOOLE_0:def 4;
end;
Lm11: for L being continuous lower-bounded Scott TopLattice,
x be Element of L holds wayabove x is open
proof
let L be continuous lower-bounded Scott TopLattice, x be Element of L;
set W = wayabove x;
W is inaccessible
proof
let D be non empty directed Subset of L;
assume sup D in W;
then x << sup D by WAYBEL_3:8;
then consider d being Element of L such that
A1: d in D and
A2: x << d by WAYBEL_4:53;
d in W by A2;
hence thesis by A1,XBOOLE_0:3;
end;
hence thesis by WAYBEL11:def 4;
end;
Lm12: for L being lower-bounded continuous Scott TopLattice, p be Element of L
holds { wayabove q where q is Element of L: q << p } is Basis of p
proof
let L be lower-bounded continuous Scott TopLattice, p be Element of L;
set X = { wayabove q where q is Element of L: q << p };
X c= bool the carrier of L
proof
let e be object;
assume e in X;
then ex q being Element of L st e = wayabove q & q << p;
hence thesis;
end;
then reconsider X as Subset-Family of L;
X is Basis of p
proof
A1: X is open
proof
let e be Subset of L;
assume e in X;
then consider q being Element of L such that
A2: e = wayabove q and q << p;
wayabove q is open by Lm11;
hence thesis by A2;
end;
X is p-quasi_basis
proof
for Y being set st Y in X holds p in Y
proof
let e be set;
assume e in X;
then ex q being Element of L st e = wayabove q & q << p;
hence thesis;
end;
hence p in Intersect X by SETFAM_1:43;
let S be Subset of L such that
A3: S is open and
A4: p in S;
consider u being Element of L such that
A5: u << p and
A6: u in S by A3,A4,Lm10;
take V = wayabove u;
thus V in X by A5;
A7: S is upper by A3,WAYBEL11:def 4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by A6,A7,WAYBEL11:42;
hence thesis by A8;
end;
hence thesis by A1;
end;
hence thesis;
end;
Lm13: for T being lower-bounded continuous Scott TopLattice holds
the set of all wayabove x where x is Element of T is Basis of T
proof
let T be lower-bounded continuous Scott TopLattice;
set B = the set of all wayabove x where x is Element of T;
A1: B c= the topology of T
proof
let e be object;
assume e in B;
then consider x being Element of T such that
A2: e = wayabove x;
wayabove x is open by Lm11;
hence thesis by A2;
end;
then reconsider P = B as Subset-Family of T by XBOOLE_1:1;
for x being Point of T ex B being Basis of x st B c= P
proof
let x be Point of T;
reconsider p = x as Element of T;
reconsider A =
{ wayabove q where q is Element of T: q << p } as Basis of x by Lm12;
take A;
let u be object;
assume u in A;
then ex q being Element of T st u = wayabove q & q << p;
hence thesis;
end;
hence thesis by A1,YELLOW_8:14;
end;
Lm14: for T being lower-bounded continuous Scott TopLattice,
S being Subset of T
holds Int S = union {wayabove x where x is Element of T: wayabove x c= S}
proof
let T be lower-bounded continuous Scott TopLattice, S be Subset of T;
set B = the set of all wayabove x where x is Element of T;
set I = { G where G is Subset of T: G in B & G c= S };
set P = {wayabove x where x is Element of T: wayabove x c= S};
A1: I = P
proof
thus I c= P
proof
let e be object;
assume e in I;
then consider G being Subset of T such that
A2: e = G and
A3: G in B and
A4: G c= S;
ex x being Element of T st G = wayabove x by A3;
hence thesis by A2,A4;
end;
let e be object;
assume e in P;
then consider x being Element of T such that
A5: e = wayabove x and
A6: wayabove x c= S;
wayabove x in B;
hence thesis by A5,A6;
end;
B is Basis of T by Lm13;
hence thesis by A1,YELLOW_8:11;
end;
Lm15: for S, T being continuous lower-bounded Scott TopLattice,
f being Function of S, T holds
( ( for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st
w << x & y << f.w ) implies f is continuous )
proof
let S, T be continuous lower-bounded Scott TopLattice;
let f be Function of S, T;
assume
A1: for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w;
A2: [#]T <> {};
now
let U1 be Subset of T;
assume
A3: U1 is open;
set U19 = U1;
A4: U19 is upper by A3,WAYBEL11:def 4;
reconsider fU = f"U1 as Subset of S;
A5: Int fU c= fU by TOPS_1:16;
fU c= Int fU
proof
let xx be object;
assume
A6: xx in fU;
then reconsider x = xx as Element of S;
A7: f.x in U1 by A6,FUNCT_1:def 7;
reconsider p = f.x as Element of T;
consider u being Element of T such that
A8: u << p and
A9: u in U19 by A3,A7,Lm10;
consider w being Element of S such that
A10: w << x and
A11: u << f.w by A1,A8;
f.:(wayabove w) c= U1
proof
let h be object;
assume h in f.:(wayabove w);
then consider z be object such that
A12: z in dom f and
A13: z in wayabove w and
A14: h = f.z by FUNCT_1:def 6;
reconsider z as Element of S by A12;
w << z by A13,WAYBEL_3:8;
then u << f.z by A1,A11;
then u <= f.z by WAYBEL_3:1;
hence thesis by A4,A9,A14;
end;
then
A15: f"(f.:(wayabove w)) c= f"U1 by RELAT_1:143;
wayabove w c= f"(f.:(wayabove w)) by FUNCT_2:42;
then
A16: wayabove w c= f"U1 by A15;
A17: Int
fU = union {wayabove g where g is Element of S : wayabove g c= fU} by Lm14;
A18: x in wayabove w by A10;
wayabove w in {wayabove g where g is Element of S : wayabove g c= fU
} by A16;
hence thesis by A17,A18,TARSKI:def 4;
end;
hence f"U1 is open by A5,XBOOLE_0:def 10;
end;
hence f is continuous by A2,TOPS_2:43;
end;
begin :: Necessary and sufficient conditions of Scott-continuity
:: Proposition 2.1, p. 112, (1) <=> (2)
theorem
for S, T being complete Scott TopLattice, f being Function of S, T holds
f is continuous iff for N be net of S holds f.(lim_inf N) <= lim_inf (f*N)
by Lm4,Lm8,Lm9;
:: Proposition 2.1, p. 112, (1) <=> (3)
theorem Th22:
for S, T being complete Scott TopLattice, f being Function of S, T holds
f is continuous iff f is directed-sups-preserving
proof
let S, T be complete Scott TopLattice, f be Function of S, T;
thus f is continuous implies f is directed-sups-preserving
proof
assume f is continuous;
then for N be net of S holds f.(lim_inf N) <= lim_inf (f*N) by Lm9;
hence thesis by Lm8;
end;
thus thesis by Lm4;
end;
registration
let S, T be complete Scott TopLattice;
cluster continuous -> directed-sups-preserving for Function of S, T;
coherence by Th22;
cluster directed-sups-preserving -> continuous for Function of S, T;
coherence by Th22;
end;
Lm16: for S, T being continuous complete Scott TopLattice,
f being 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) ) implies
f is directed-sups-preserving)
proof
let S, T be continuous complete Scott TopLattice, f be Function of S, T;
assume for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T);
then for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w by Th14;
then f is continuous by Lm15;
hence thesis;
end;
:: Proposition 2.1, p. 112, (1) <=> (4)
theorem Th23:
for S, T being continuous complete Scott TopLattice,
f being Function of S, T holds ( f is continuous iff
for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w )
proof
let S, T be continuous complete Scott TopLattice, f be Function of S, T;
hereby
assume f is continuous;
then for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) by Th12;
hence for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w by Th14;
end;
thus thesis by Lm15;
end;
:: Proposition 2.1, p. 112, (1) <=> (5)
theorem Th24:
for S, T being continuous complete Scott TopLattice,
f being Function of S, T holds ( f is continuous iff
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 continuous complete Scott TopLattice, f be Function of S, T;
thus f is continuous implies for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) by Th12;
assume for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T);
then f is directed-sups-preserving by Lm16;
hence thesis;
end;
Lm17: for S, T being complete Scott TopLattice, f being Function of S, T holds
S is algebraic & T is algebraic implies
( ( for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w ) implies
for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j) )
proof
let S, T be complete Scott TopLattice, f be Function of S, T;
assume that
A1: S is algebraic and
A2: T is algebraic;
A3: S is continuous by A1,WAYBEL_8:7;
A4: T is continuous by A2,WAYBEL_8:7;
assume
A5: for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w;
then
A6: f is continuous by A3,A4,Th23;
let x be Element of S, k be Element of T;
assume
A7: k in the carrier of CompactSublatt T;
hereby
assume k <= f.x;
then k << f.x by A7,WAYBEL_8:1;
then consider w being Element of S such that
A8: w << x and
A9: k << f.w by A5;
consider w1 being Element of S such that
A10: w1 in the carrier of CompactSublatt S and
A11: w <= w1 and
A12: w1 <= x by A1,A8,WAYBEL_8:7;
A13: k <= f.w by A9,WAYBEL_3:1;
take w1;
thus w1 in the carrier of CompactSublatt S by A10;
thus w1 <= x by A12;
f.w <= f.w1 by A6,A11,WAYBEL_1:def 2;
hence k <= f.w1 by A13,ORDERS_2:3;
end;
given j being Element of S such that
j in the carrier of CompactSublatt S and
A14: j <= x and
A15: k <= f.j;
f is continuous by A3,A4,A5,Lm15;
then f.j <= f.x by A14,WAYBEL_1:def 2;
hence thesis by A15,ORDERS_2:3;
end;
Lm18: for S, T being complete Scott TopLattice, f being Function of S, T holds
T is algebraic implies
( ( for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j) ) implies
for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w )
proof
let S, T be complete Scott TopLattice, f be Function of S, T;
assume that
A1: T is algebraic;
assume
A2: for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j);
let x be Element of S, y be Element of T;
hereby
assume y << f.x;
then consider w being Element of T such that
A3: w in the carrier of CompactSublatt T and
A4: y <= w and
A5: w <= f.x by A1,WAYBEL_8:7;
consider j being Element of S such that
A6: j in the carrier of CompactSublatt S and
A7: j <= x and
A8: w <= f.j by A2,A3,A5;
take j;
thus j << x by A6,A7,WAYBEL_8:1;
thus y << f.j by A3,A4,A8,WAYBEL_8:1;
end;
given w being Element of S such that
A9: w << x and
A10: y << f.w;
consider h being Element of T such that
A11: h in the carrier of CompactSublatt T and
A12: y <= h and
A13: h <= f.w by A1,A10,WAYBEL_8:7;
consider j being Element of S such that
A14: j in the carrier of CompactSublatt S and
A15: j <= w and
A16: h <= f.j by A2,A11,A13;
j << x by A9,A15,WAYBEL_3:2;
then j <= x by WAYBEL_3:1;
then h <= f.x by A2,A11,A14,A16;
hence thesis by A11,A12,WAYBEL_8:1;
end;
Lm19: for S, T being complete Scott TopLattice, f being Function of S, T holds
S is algebraic & T is algebraic implies ( ( for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) ) implies
for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T) )
proof
let S, T be complete Scott TopLattice, f be Function of S, T;
assume that
A1: S is algebraic and
A2: T is algebraic;
A3: S is continuous by A1,WAYBEL_8:7;
A4: T is continuous by A2,WAYBEL_8:7;
assume
A5: for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T);
let x be Element of S;
A6: the carrier of S c= dom f by FUNCT_2:def 1;
defpred P[Element of S] means $1 <= x & $1 is compact;
deffunc A(Element of S) = $1;
A7: f.:{ A(w) where w is Element of S : P[w] } =
{ f.A(w) where w is Element of S : P[w] } from FuncFraenkelS(A6);
A8: f.:{ w where w is Element of S : w <= x & w is compact } =
f.:compactbelow x by WAYBEL_8:def 2;
reconsider D = compactbelow x as non empty directed Subset of S
by A1,WAYBEL_8:def 4;
f is directed-sups-preserving by A3,A4,A5,Lm16;
then
A9: f preserves_sup_of D;
A10: ex_sup_of D,S by YELLOW_0:17;
S is satisfying_axiom_K by A1,WAYBEL_8:def 4;
then f.x = f.sup D by WAYBEL_8:def 3
.= "\/"({ f.w where w is Element of S : w <= x & w is compact },T)
by A7,A8,A9,A10;
hence thesis;
end;
theorem Th25:
for S being LATTICE, T being complete LATTICE,
f being Function of S, T holds ( for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T ) )
implies f is monotone
proof
let S be LATTICE, T be complete LATTICE, f be Function of S, T;
assume
A1: for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T );
thus f is monotone
proof
let X,Y be Element of S;
assume X <= Y;
then
A2: compactbelow X c= compactbelow Y by WAYBEL13:1;
A3: f.X = "\/"
({ f.w where w is Element of S : w <= X & w is compact },T) by A1;
A4: f.Y = "\/"
({ f.w where w is Element of S : w <= Y & w is compact },T) by A1;
A5: the carrier of S c= dom f by FUNCT_2:def 1;
defpred P[Element of S] means $1 <= X & $1 is compact;
defpred Q[Element of S] means $1 <= Y & $1 is compact;
deffunc A(Element of S) = $1;
f.:{ A(w) where w is Element of S : P[w]} =
{ f.A(w) where w is Element of S : P[w]} from FuncFraenkelSL(A5);
then
A6: f.X = "\/"(f.:compactbelow X,T) by A3,WAYBEL_8:def 2;
f.:{ A(w) where w is Element of S : Q[w]} =
{ f.A(w) where w is Element of S : Q[w]} from FuncFraenkelSL(A5);
then
A7: f.Y = "\/"(f.:compactbelow Y,T) by A4,WAYBEL_8:def 2;
A8: ex_sup_of f.:compactbelow X,T by YELLOW_0:17;
ex_sup_of f.:compactbelow Y,T by YELLOW_0:17;
hence thesis by A2,A6,A7,A8,RELAT_1:123,YELLOW_0:34;
end;
end;
theorem Th26:
for S, T being complete Scott TopLattice, f being Function of S, T holds
(( for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T ) )
implies 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 Scott TopLattice, f be Function of S, T;
assume
A1: for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T );
then
A2: f is monotone by Th25;
let x be Element of S;
A3: f.x = "\/"
({ f.w where w is Element of S : w <= x & w is compact },T ) by A1;
set FW = { f.w where w is Element of S : w <= x & w is compact };
set FX = { f.w where w is Element of S : w << x };
set fx = f.x;
A4: FW c= FX
proof
let a be object;
assume a in { f.w where w is Element of S : w <= x & w is compact };
then consider w be Element of S such that
A5: a = f.w and
A6: w <= x and
A7: w is compact;
w << w by A7;
then w << x by A6,WAYBEL_3:2;
hence thesis by A5;
end;
A8: fx is_>=_than FX
proof
let b be Element of T;
assume b in FX;
then consider ww be Element of S such that
A9: b = f.ww and
A10: ww << x;
ww <= x by A10,WAYBEL_3:1;
hence thesis by A2,A9;
end;
for b being Element of T st b is_>=_than FX holds fx <= b
proof
let b be Element of T;
assume b is_>=_than FX;
then b is_>=_than FW by A4;
hence thesis by A3,YELLOW_0:32;
end;
hence thesis by A8,YELLOW_0:30;
end;
:: Proposition 2.1, p. 112, (1) <=> (6)
theorem
for S, T being complete Scott TopLattice, f being Function of S, T holds
S is algebraic & T is algebraic implies ( f is continuous iff
for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j) )
proof
let S, T be complete Scott TopLattice, f be Function of S, T;
assume that
A1: S is algebraic and
A2: T is algebraic;
A3: S is continuous by A1,WAYBEL_8:7;
A4: T is continuous by A2,WAYBEL_8:7;
hereby
assume f is continuous;
then for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st
w << x & y << f.w by A3,A4,Th23;
hence for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j) by A1,A2,Lm17;
end;
assume for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j);
then for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w by A2,Lm18;
hence thesis by A3,A4,Th23;
end;
:: Proposition 2.1, p. 112, (1) <=> (7)
theorem
for S, T being complete Scott TopLattice, f being Function of S, T holds
S is algebraic & T is algebraic implies ( f is continuous iff
for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T ) )
proof
let S, T be complete Scott TopLattice, f be Function of S, T;
assume that
A1: S is algebraic and
A2: T is algebraic;
A3: S is continuous by A1,WAYBEL_8:7;
A4: T is continuous by A2,WAYBEL_8:7;
hereby
assume f is continuous;
then for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) by A3,A4,Th24;
hence for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T )
by A1,A2,Lm19;
end;
assume for x being Element of S holds f.x = "\/"
({ f.w where w is Element of S : w <= x & w is compact },T );
then for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) by Th26;
hence thesis by A3,A4,Th24;
end;
theorem
for S, T being up-complete Scott non empty
reflexive transitive antisymmetric TopSpace-like TopRelStr,
f be Function of S, T holds
f is directed-sups-preserving implies f is continuous by Lm4;