:: Lawson Topology in Continuous Lattices
:: by Grzegorz Bancerek
::
:: Received July 12, 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 WAYBEL_0, LATTICES, FUNCT_1, FINSET_1, SUBSET_1, STRUCT_0,
FUNCOP_1, YELLOW_0, XBOOLE_0, RELAT_1, ORDINAL2, TARSKI, SEQM_3,
XXREAL_0, LATTICE3, ORDERS_2, REWRITE1, CAT_1, FUNCT_3, EQREL_1,
WELLORD1, WAYBEL_5, PRE_TOPC, ORDINAL1, CONNSP_2, TOPS_1, RCOMP_1,
RELAT_2, WAYBEL_9, ARYTM_0, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1,
YELLOW_9, PROB_1, YELLOW_2, PRELAMB, WAYBEL21;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, FINSET_1, TOLER_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1, ORDERS_2, LATTICE3, ORDERS_3,
YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3, WAYBEL_5, YELLOW_6, YELLOW_7,
WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL17, WAYBEL19;
constructors TOLER_1, TOPS_1, NATTRA_1, BORSUK_1, CANTOR_1, TOPS_2, ORDERS_3,
YELLOW_2, WAYBEL_3, WAYBEL17, YELLOW_9, WAYBEL19, COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, PRE_TOPC,
LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2, YELLOW_6, WAYBEL_9, WAYBEL10,
WAYBEL17, YELLOW_9, WAYBEL19, TOPS_1, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_6,
XBOOLE_0;
equalities LATTICE3, YELLOW_0, WAYBEL_0, WELLORD1, RELAT_1, STRUCT_0;
expansions TARSKI, LATTICE3, YELLOW_0, WAYBEL_0, XBOOLE_0;
theorems YELLOW_0, WAYBEL_0, WAYBEL_6, PRE_TOPC, FUNCOP_1, RELAT_1, FUNCT_2,
TOPS_1, TOPS_2, ZFMISC_1, CONNSP_2, WAYBEL_9, YELLOW_9, FUNCT_1,
WAYBEL_1, YELLOW_6, WAYBEL19, SETWISEO, FUNCT_3, TARSKI, LATTICE3,
WAYBEL11, WAYBEL17, ORDERS_2, YELLOW_2, WEIERSTR, COMPTS_1, WAYBEL10,
YELLOW_7, YELLOW_4, WAYBEL20, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, FINSET_1, LATTICE3, XBOOLE_0;
begin :: Semilattice homomorphism and inheritance
definition
let S,T be Semilattice such that
A1: S is upper-bounded implies T is upper-bounded;
mode SemilatticeHomomorphism of S,T -> Function of S,T means
:Def1:
for X being finite Subset of S holds it preserves_inf_of X;
existence
proof
reconsider f = (the carrier of S) --> Top T as Function of S,T;
take f;
let X be finite Subset of S such that
A2: ex_inf_of X,S;
per cases;
suppose
A3: X = {};
then
A4: f.:X = {};
hence ex_inf_of f.:X,T by A1,A2,A3,WAYBEL20:5,YELLOW_0:43;
thus f.inf X = inf (f.:X) by A4,FUNCOP_1:7;
end;
suppose X <> {};
then reconsider A = X as non empty Subset of S;
set a = the Element of A;
reconsider a as Element of S;
A5: dom f = the carrier of S by FUNCOP_1:13;
f.a = Top T by FUNCOP_1:7;
then Top T in f.:X by A5,FUNCT_1:def 6;
then
A6: {Top T} c= f.:X by ZFMISC_1:31;
f.:X c= {Top T} by FUNCOP_1:81;
then
A7: {Top T} = f.:X by A6;
f.inf X = Top T by FUNCOP_1:7;
hence thesis by A7,YELLOW_0:38,39;
end;
end;
end;
registration
let S,T be Semilattice;
cluster meet-preserving -> monotone for Function of S,T;
coherence
proof
let f be Function of S,T;
assume
A1: f is meet-preserving;
let x,y be Element of S;
assume x <= y;
then x = x "/\" y by YELLOW_0:25;
then f.x = (f.x) "/\" (f.y) by A1,WAYBEL_6:1;
hence thesis by YELLOW_0:25;
end;
end;
registration
let S be Semilattice, T be upper-bounded Semilattice;
cluster -> meet-preserving for SemilatticeHomomorphism of S,T;
coherence
by Def1;
end;
theorem
for S,T being upper-bounded Semilattice
for f being SemilatticeHomomorphism of S,T holds f.Top S = Top T
proof
let S, T be upper-bounded Semilattice;
let f be SemilatticeHomomorphism of S,T;
A1: f preserves_inf_of {}S by Def1;
ex_inf_of {}S,S by YELLOW_0:43;
then f.inf {}S = inf (f.:{}S) by A1;
hence thesis;
end;
theorem Th2:
for S,T being Semilattice, f being Function of S,T st f is meet-preserving
for X being finite non empty Subset of S holds f preserves_inf_of X
proof
let S,T be Semilattice, f be Function of S,T such that
A1: f is meet-preserving;
let X be finite non empty Subset of S such that ex_inf_of X,S;
A2: X is finite;
defpred P[set] means $1 <> {} implies ex_inf_of $1, S & ex_inf_of f.:$1, T &
inf (f.:$1) = f."/\"($1,S);
A3: P[{}];
A4: now
let y,x be set such that
A5: y in X and x c= X and
A6: P[x];
thus P[x \/ {y}]
proof
assume x \/ {y} <> {};
reconsider y9 = y as Element of S by A5;
set fy = f.y9;
A7: ex_inf_of {fy}, T by YELLOW_0:38;
A8: inf {fy} = fy by YELLOW_0:39;
A9: ex_inf_of {y9}, S by YELLOW_0:38;
A10: inf {y9} = y by YELLOW_0:39;
thus ex_inf_of x \/ {y}, S by A6,A9,YELLOW_2:4;
dom f = the carrier of S by FUNCT_2:def 1;
then
A11: Im(f,y) = {fy} by FUNCT_1:59;
then
A12: f.:(x \/ {y}) = (f.:x) \/ {fy} by RELAT_1:120;
hence ex_inf_of f.:(x \/ {y}), T by A6,A7,A11,YELLOW_2:4;
per cases;
suppose x = {};
hence thesis by A8,A11,YELLOW_0:39;
end;
suppose
A13: x <> {};
hence "/\"(f.:(x \/ {y}), T)
= (f."/\"(x, S)) "/\" fy by A6,A7,A8,A12,YELLOW_2:4
.= f.("/\"(x, S)"/\" y9) by A1,WAYBEL_6:1
.= f."/\"(x \/ {y}, S) by A6,A9,A10,A13,YELLOW_2:4;
end;
end;
end;
P[X] from FINSET_1:sch 2(A2,A3,A4);
hence thesis;
end;
theorem
for S,T being upper-bounded Semilattice, f being meet-preserving Function
of S, T st f.Top S = Top T holds f is SemilatticeHomomorphism of S,T
proof
let S,T be upper-bounded Semilattice, f be meet-preserving Function of S,T
such that
A1: f.Top S = Top T;
thus S is upper-bounded implies T is upper-bounded;
let X be finite Subset of S;
A2: ex_inf_of f.:{}, T by YELLOW_0:43;
X = {} or f preserves_inf_of X by Th2;
hence thesis by A1,A2;
end;
theorem Th4:
for S,T being Semilattice, f being Function of S,T st f is meet-preserving &
for X being filtered non empty Subset of S holds f preserves_inf_of X
for X being non empty Subset of S holds f preserves_inf_of X
proof
let S,T be Semilattice, f be Function of S,T such that
A1: f is meet-preserving and
A2: for X being non empty filtered Subset of S holds f preserves_inf_of X;
let X be non empty Subset of S such that
A3: ex_inf_of X,S;
defpred P[object] means
ex Y being non empty finite Subset of X st ex_inf_of Y, S & $1 = "/\"(Y,S);
consider Z being set such that
A4: for x being object holds x in Z iff x in the carrier of S & P[x]
from XBOOLE_0:sch 1;
set a = the Element of X;
reconsider a9 = a as Element of S;
A5: ex_inf_of {a}, S by YELLOW_0:38;
A6: inf {a9} = a by YELLOW_0:39;
Z c= the carrier of S
by A4;
then reconsider Z as non empty Subset of S by A4,A5,A6;
A7: now
let Y be finite Subset of X;
Y is Subset of S by XBOOLE_1:1;
hence Y <> {} implies ex_inf_of Y, S by YELLOW_0:55;
end;
A8: now
let Y be finite Subset of X;
reconsider Y9 = Y as Subset of S by XBOOLE_1:1;
assume
A9: Y <> {};
then ex_inf_of Y9, S by YELLOW_0:55;
hence "/\"(Y,S) in Z by A4,A9;
end;
A10: now
let x be Element of S;
assume x in Z;
then ex Y being non empty finite Subset of X st ex_inf_of Y,S & x = "/\"
(Y,S) by A4;
hence ex Y being finite Subset of X st ex_inf_of Y,S & x = "/\"(Y,S);
end;
then
A11: Z is filtered by A7,A8,WAYBEL_0:56;
A12: ex_inf_of Z, S by A3,A7,A8,A10,WAYBEL_0:58;
A13: f preserves_inf_of Z by A2,A11;
then
A14: ex_inf_of f.:Z,T by A12;
A15: inf (f.:Z) = f.inf Z by A12,A13;
A16: inf Z = inf X by A3,A7,A8,A10,WAYBEL_0:59;
X c= Z
proof
let x be object;
assume
A17: x in X;
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;
reconsider x as Element of S by A17;
Y is Subset of S by XBOOLE_1:1;
then
A18: ex_inf_of Y, S by YELLOW_0:55;
x = "/\"(Y,S) by YELLOW_0:39;
hence thesis by A4,A18;
end;
then
A19: f.:X c= f.:Z by RELAT_1:123;
A20: f.:Z is_>=_than f.inf X by A14,A15,A16,YELLOW_0:31;
A21: f.:X is_>=_than f.inf X
by A19,A20;
A22: now
let b be Element of T;
assume
A23: f.:X is_>=_than b;
f.:Z is_>=_than b
proof
let a be Element of T;
assume a in f.:Z;
then consider x being object such that
x in dom f and
A24: x in Z and
A25: a = f.x by FUNCT_1:def 6;
consider Y being non empty finite Subset of X such that
A26: ex_inf_of Y, S and
A27: x = "/\"(Y,S) by A4,A24;
reconsider Y as Subset of S by XBOOLE_1:1;
A28: f.:Y c= f.:X by RELAT_1:123;
A29: f preserves_inf_of Y by A1,Th2;
A30: b is_<=_than f.:Y by A23,A28;
A31: a = "/\"(f.:Y,T) by A25,A26,A27,A29;
ex_inf_of f.:Y, T by A26,A29;
hence thesis by A30,A31,YELLOW_0:def 10;
end;
hence f.inf X >= b by A14,A15,A16,YELLOW_0:31;
end;
hence ex_inf_of f.:X,T by A21,YELLOW_0:16;
hence inf (f.:X) = f.inf X by A21,A22,YELLOW_0:def 10;
end;
theorem Th5:
for S,T being Semilattice, f being Function of S,T st f is infs-preserving
holds f is SemilatticeHomomorphism of S,T
proof
let S,T be Semilattice, f be Function of S,T such that
A1: f is infs-preserving;
reconsider e = {} as Subset of S by XBOOLE_1:2;
hereby
assume S is upper-bounded;
then
A2: ex_inf_of e, S by YELLOW_0:43;
f preserves_inf_of e by A1;
then
A3: ex_inf_of f.:e, T by A2;
f.:e = {};
hence T is upper-bounded by A3,WAYBEL20:5;
end;
let X be finite Subset of S;
thus thesis by A1;
end;
theorem Th6:
for S1,T1,S2,T2 being non empty RelStr
st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
for f1 being Function of S1,T1, f2 being Function of S2,T2 st f1 = f2 holds
(f1 is infs-preserving implies f2 is infs-preserving) &
(f1 is directed-sups-preserving implies f2 is directed-sups-preserving)
proof
let S1,T1,S2,T2 be non empty RelStr such that
A1: the RelStr of S1 = the RelStr of S2 and
A2: the RelStr of T1 = the RelStr of T2;
let f1 be Function of S1,T1, f2 be Function of S2,T2 such that
A3: f1 = f2;
thus f1 is infs-preserving implies f2 is infs-preserving
by A1,A2,A3,WAYBEL_0:65;
assume
A4: for X being Subset of S1 st X is non empty directed
holds f1 preserves_sup_of X;
let X be Subset of S2;
reconsider Y = X as Subset of S1 by A1;
assume X is non empty directed;
then f1 preserves_sup_of Y by A1,A4,WAYBEL_0:3;
hence thesis by A1,A2,A3,WAYBEL_0:65;
end;
theorem
for S1,T1,S2,T2 being non empty RelStr
st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
for f1 being Function of S1,T1, f2 being Function of S2,T2 st f1 = f2 holds
(f1 is sups-preserving implies f2 is sups-preserving) &
(f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving)
proof
let S1,T1,S2,T2 be non empty RelStr such that
A1: the RelStr of S1 = the RelStr of S2 and
A2: the RelStr of T1 = the RelStr of T2;
let f1 be Function of S1,T1, f2 be Function of S2,T2 such that
A3: f1 = f2;
thus f1 is sups-preserving implies f2 is sups-preserving
by A1,A2,A3,WAYBEL_0:65;
assume
A4: for X being Subset of S1 st X is non empty filtered
holds f1 preserves_inf_of X;
let X be Subset of S2;
reconsider Y = X as Subset of S1 by A1;
assume X is non empty filtered;
then f1 preserves_inf_of Y by A1,A4,WAYBEL_0:4;
hence thesis by A1,A2,A3,WAYBEL_0:65;
end;
theorem Th8:
for T being complete LATTICE
for S being infs-inheriting full non empty SubRelStr of T
holds incl(S,T) is infs-preserving
proof
let T be complete LATTICE;
let S be infs-inheriting full non empty SubRelStr of T;
set f = incl(S,T);
let X be Subset of S;
assume ex_inf_of X, S;
thus ex_inf_of f.:X, T by YELLOW_0:17;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then
A1: f = id the carrier of S by YELLOW_9:def 1;
then
A2: f.:X = X by FUNCT_1:92;
A3: ex_inf_of X, T by YELLOW_0:17;
A4: f.inf X = inf X by A1;
"/\"(X,T) in the carrier of S by A3,YELLOW_0:def 18;
hence thesis by A2,A3,A4,YELLOW_0:63;
end;
theorem
for T being complete LATTICE
for S being sups-inheriting full non empty SubRelStr of T
holds incl(S,T) is sups-preserving
proof
let T be complete LATTICE;
let S be sups-inheriting full non empty SubRelStr of T;
set f = incl(S,T);
let X be Subset of S;
assume ex_sup_of X, S;
thus ex_sup_of f.:X, T by YELLOW_0:17;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then
A1: f = id the carrier of S by YELLOW_9:def 1;
then
A2: f.:X = X by FUNCT_1:92;
A3: ex_sup_of X, T by YELLOW_0:17;
A4: f.sup X = sup X by A1;
"\/"(X,T) in the carrier of S by A3,YELLOW_0:def 19;
hence thesis by A2,A3,A4,YELLOW_0:64;
end;
theorem Th10:
for T being up-complete non empty Poset
for S being directed-sups-inheriting full non empty SubRelStr of T
holds incl(S,T) is directed-sups-preserving
proof
let T be up-complete non empty Poset;
let S be directed-sups-inheriting full non empty SubRelStr of T;
set f = incl(S,T);
let X be Subset of S;
assume that
A1: X is non empty directed and ex_sup_of X, S;
reconsider X9 = X as non empty directed Subset of T by A1,YELLOW_2:7;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then
A2: f = id the carrier of S by YELLOW_9:def 1;
then
A3: f.:X = X9 by FUNCT_1:92;
A4: f.sup X = sup X by A2;
thus ex_sup_of f.:X, T by A3,WAYBEL_0:75;
hence thesis by A1,A3,A4,WAYBEL_0:7;
end;
theorem
for T being complete LATTICE
for S being filtered-infs-inheriting full non empty SubRelStr of T
holds incl(S,T) is filtered-infs-preserving
proof
let T be complete LATTICE;
let S be filtered-infs-inheriting full non empty SubRelStr of T;
set f = incl(S,T);
let X be Subset of S;
assume that
A1: X is non empty filtered and ex_inf_of X, S;
thus ex_inf_of f.:X, T by YELLOW_0:17;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then
A2: f = id the carrier of S by YELLOW_9:def 1;
then
A3: f.:X = X by FUNCT_1:92;
A4: ex_inf_of X, T by YELLOW_0:17;
f.inf X = inf X by A2;
hence thesis by A1,A3,A4,WAYBEL_0:6;
end;
theorem Th12:
for T1,T2,R being RelStr, S being SubRelStr of T1
st the RelStr of T1 = the RelStr of T2 & the RelStr of S = the RelStr of R
holds R is SubRelStr of T2 & (S is full implies R is full SubRelStr of T2)
proof
let T,T2,R be RelStr, S be SubRelStr of T such that
A1: the RelStr of T = the RelStr of T2 and
A2: the RelStr of S = the RelStr of R;
A3: the carrier of R c= the carrier of T2 by A1,A2,YELLOW_0:def 13;
A4: the InternalRel of R c= the InternalRel of T2 by A1,A2,YELLOW_0:def 13;
hence R is SubRelStr of T2 by A3,YELLOW_0:def 13;
assume the InternalRel of S = (the InternalRel of T)|_2 the carrier of S;
hence thesis by A1,A2,A3,A4,YELLOW_0:def 13,def 14;
end;
theorem Th13:
for T being non empty RelStr holds
T is infs-inheriting sups-inheriting full SubRelStr of T
proof
let T be non empty RelStr;
reconsider R = T as full SubRelStr of T by YELLOW_6:6;
A1: R is infs-inheriting;
R is sups-inheriting;
hence thesis by A1;
end;
registration
let T be complete LATTICE;
cluster complete for CLSubFrame of T;
existence
proof
T is infs-inheriting sups-inheriting full SubRelStr of T by Th13;
hence thesis;
end;
end;
theorem Th14:
for T being Semilattice for S being full non empty SubRelStr of T
holds S is meet-inheriting iff
for X being finite non empty Subset of S holds "/\"
(X, T) in the carrier of S
proof
let T be Semilattice;
let S be full non empty SubRelStr of T;
hereby
assume
A1: S is meet-inheriting;
let X be finite non empty Subset of S;
A2: X is finite;
defpred P[set] means $1 <> {} implies "/\"($1, T) in the carrier of S;
A3: P[{}];
A4: now
let y,x be set;
assume that
A5: y in X and
A6: x c= X and
A7: P[x];
thus P[x \/ {y}]
proof
assume x \/ {y} <> {};
reconsider y9 = y as Element of S by A5;
reconsider z = y9 as Element of T by YELLOW_0:58;
A8: x c= the carrier of S by A6,XBOOLE_1:1;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider x9 = x as finite Subset of T
by A6,A8,XBOOLE_1:1;
A9: ex_inf_of {z}, T by YELLOW_0:38;
A10: inf {z} = y9 by YELLOW_0:39;
now
assume
A11: x9 <> {};
then ex_inf_of x9, T by YELLOW_0:55;
then
A12: inf (x9 \/ {z}) = (inf x9 )"/\"z by A9,A10,YELLOW_2:4;
ex_inf_of {inf x9, z}, T by YELLOW_0:21;
then inf {inf x9, z} in the carrier of S by A1,A7,A11;
hence inf (x9 \/ {z}) in the carrier of S by A12,YELLOW_0:40;
end;
hence thesis by A10;
end;
end;
P[X] from FINSET_1:sch 2(A2,A3,A4);
hence "/\"(X, T) in the carrier of S;
end;
assume
A13: for X being finite non empty Subset of S holds "/\"
(X, T) in the carrier of S;
let x,y be Element of T;
assume that
A14: x in the carrier of S and
A15: y in the carrier of S;
{x,y} c= the carrier of S by A14,A15,ZFMISC_1:32;
hence thesis by A13;
end;
theorem Th15:
for T being sup-Semilattice for S being full non empty SubRelStr of T
holds S is join-inheriting iff
for X being finite non empty Subset of S holds "\/"
(X, T) in the carrier of S
proof
let T be sup-Semilattice;
let S be full non empty SubRelStr of T;
hereby
assume
A1: S is join-inheriting;
let X be finite non empty Subset of S;
A2: X is finite;
defpred P[set] means $1 <> {} implies "\/"($1, T) in the carrier of S;
A3: P[{}];
A4: now
let y,x be set;
assume that
A5: y in X and
A6: x c= X and
A7: P[x];
reconsider y9 = y as Element of S by A5;
reconsider z = y9 as Element of T by YELLOW_0:58;
thus P[x \/ {y}]
proof
assume x \/ {y} <> {};
A8: x c= the carrier of S by A6,XBOOLE_1:1;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider x9 = x as finite Subset of T
by A6,A8,XBOOLE_1:1;
A9: ex_sup_of {z}, T by YELLOW_0:38;
A10: sup {z} = y9 by YELLOW_0:39;
now
assume
A11: x9 <> {};
then ex_sup_of x9, T by YELLOW_0:54;
then
A12: sup (x9 \/ {z}) = (sup x9 ) "\/"z by A9,A10,YELLOW_2:3;
ex_sup_of {sup x9, z}, T by YELLOW_0:20;
then sup {sup x9, z} in the carrier of S by A1,A7,A11;
hence sup (x9 \/ {z}) in the carrier of S by A12,YELLOW_0:41;
end;
hence thesis by A10;
end;
end;
P[X] from FINSET_1:sch 2(A2,A3,A4);
hence "\/"(X, T) in the carrier of S;
end;
assume
A13: for X being finite non empty Subset of S holds "\/"
(X, T) in the carrier of S;
let x,y be Element of T;
assume that
A14: x in the carrier of S and
A15: y in the carrier of S;
{x,y} c= the carrier of S by A14,A15,ZFMISC_1:32;
hence thesis by A13;
end;
theorem Th16:
for T being upper-bounded Semilattice
for S being meet-inheriting full non empty SubRelStr of T
st Top T in the carrier of S & S is filtered-infs-inheriting
holds S is infs-inheriting
proof
let T be upper-bounded Semilattice;
let S be meet-inheriting full non empty SubRelStr of T such that
A1: Top T in the carrier of S and
A2: S is filtered-infs-inheriting;
let A be Subset of S;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider C = A as Subset of T by XBOOLE_1:1;
set F = fininfs C;
assume
A3: ex_inf_of A, T;
then
A4: inf F = inf C by WAYBEL_0:60;
F c= the carrier of S
proof
let x be object;
assume x in F;
then consider Y being finite Subset of C such that
A5: x = "/\"(Y, T) and ex_inf_of Y, T;
reconsider Y as finite Subset of T by XBOOLE_1:1;
reconsider Z = Y as finite Subset of S by XBOOLE_1:1;
assume
A6: not x in the carrier of S;
then Z <> {} by A1,A5;
hence thesis by A5,A6,Th14;
end;
then reconsider G = F as non empty Subset of S;
reconsider G as filtered non empty Subset of S by WAYBEL10:23;
A7: now
let Y be finite Subset of C;
Y c= the carrier of T by XBOOLE_1:1;
hence Y <> {} implies ex_inf_of Y,T by YELLOW_0:55;
end;
A8: now
let x be Element of T;
assume x in F;
then ex Y being finite Subset of C st x = "/\"(Y,T) & ex_inf_of Y,T;
hence ex Y being finite Subset of C st ex_inf_of Y,T & x = "/\"(Y,T);
end;
now
let Y be finite Subset of C;
reconsider Z = Y as finite Subset of T by XBOOLE_1:1;
assume Y <> {};
then ex_inf_of Z, T by YELLOW_0:55;
hence "/\"(Y,T) in F;
end;
then ex_inf_of G, T by A3,A7,A8,WAYBEL_0:58;
hence thesis by A2,A4;
end;
theorem
for T being lower-bounded sup-Semilattice
for S being join-inheriting full non empty SubRelStr of T
st Bottom T in the carrier of S & S is directed-sups-inheriting
holds S is sups-inheriting
proof
let T be lower-bounded sup-Semilattice;
let S be join-inheriting full non empty SubRelStr of T such that
A1: Bottom T in the carrier of S and
A2: S is directed-sups-inheriting;
let A be Subset of S;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider C = A as Subset of T by XBOOLE_1:1;
set F = finsups C;
assume
A3: ex_sup_of A, T;
then
A4: sup F = sup C by WAYBEL_0:55;
F c= the carrier of S
proof
let x be object;
assume x in F;
then consider Y being finite Subset of C such that
A5: x = "\/"(Y, T) and ex_sup_of Y, T;
reconsider Y as finite Subset of T by XBOOLE_1:1;
reconsider Z = Y as finite Subset of S by XBOOLE_1:1;
assume
A6: not x in the carrier of S;
then Z <> {} by A1,A5;
hence thesis by A5,A6,Th15;
end;
then reconsider G = F as non empty Subset of S;
reconsider G as directed non empty Subset of S by WAYBEL10:23;
A7: now
let Y be finite Subset of C;
Y c= the carrier of T by XBOOLE_1:1;
hence Y <> {} implies ex_sup_of Y,T by YELLOW_0:54;
end;
A8: now
let x be Element of T;
assume x in F;
then ex Y being finite Subset of C st x = "\/"(Y,T) & ex_sup_of Y,T;
hence ex Y being finite Subset of C st ex_sup_of Y,T & x = "\/"(Y,T);
end;
now
let Y be finite Subset of C;
reconsider Z = Y as finite Subset of T by XBOOLE_1:1;
assume Y <> {};
then ex_sup_of Z, T by YELLOW_0:54;
hence "\/"(Y,T) in F;
end;
then ex_sup_of G, T by A3,A7,A8,WAYBEL_0:53;
hence thesis by A2,A4;
end;
theorem Th18:
for T being complete LATTICE, S being full non empty SubRelStr of T
st S is infs-inheriting holds S is complete
proof
let T be complete LATTICE, S be full non empty SubRelStr of T;
assume
A1: S is infs-inheriting;
now
let X be set;
set Y = X /\ the carrier of S;
reconsider Y as Subset of S by XBOOLE_1:17;
A2: ex_inf_of Y, T by YELLOW_0:17;
then "/\"(Y,T) in the carrier of S by A1;
then ex_inf_of Y, S by A2,YELLOW_0:63;
hence ex_inf_of X, S by YELLOW_0:50;
end;
hence thesis by YELLOW_2:25;
end;
theorem
for T being complete LATTICE, S being full non empty SubRelStr of T
st S is sups-inheriting holds S is complete
proof
let T be complete LATTICE, S be full non empty SubRelStr of T;
assume
A1: S is sups-inheriting;
now
let X be set;
set Y = X /\ the carrier of S;
reconsider Y as Subset of S by XBOOLE_1:17;
A2: ex_sup_of Y, T by YELLOW_0:17;
then "\/"(Y,T) in the carrier of S by A1;
then ex_sup_of Y, S by A2,YELLOW_0:64;
hence ex_sup_of X, S by YELLOW_0:50;
end;
hence thesis by YELLOW_2:24;
end;
theorem
for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2
st the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is infs-inheriting implies S2 is infs-inheriting
proof
let T1,T2 be non empty RelStr;
let S1 be non empty full SubRelStr of T1;
let S2 be non empty full SubRelStr of T2;
assume
A1: the RelStr of T1 = the RelStr of T2;
assume
A2: the carrier of S1 = the carrier of S2;
assume
A3: for X being Subset of S1 st ex_inf_of X,T1
holds "/\"(X,T1) in the carrier of S1;
let X be Subset of S2;
reconsider Y = X as Subset of S1 by A2;
assume
A4: ex_inf_of X,T2;
then "/\"(Y,T1) in the carrier of S1 by A1,A3,YELLOW_0:14;
hence thesis by A1,A2,A4,YELLOW_0:27;
end;
theorem
for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2
st the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is sups-inheriting implies S2 is sups-inheriting
proof
let T1,T2 be non empty RelStr;
let S1 be non empty full SubRelStr of T1;
let S2 be non empty full SubRelStr of T2;
assume
A1: the RelStr of T1 = the RelStr of T2;
assume
A2: the carrier of S1 = the carrier of S2;
assume
A3: for X being Subset of S1 st ex_sup_of X,T1
holds "\/"(X,T1) in the carrier of S1;
let X be Subset of S2;
reconsider Y = X as Subset of S1 by A2;
assume
A4: ex_sup_of X,T2;
then "\/"(Y,T1) in the carrier of S1 by A1,A3,YELLOW_0:14;
hence thesis by A1,A2,A4,YELLOW_0:26;
end;
theorem
for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2
st the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting
proof
let T1,T2 be non empty RelStr;
let S1 be non empty full SubRelStr of T1;
let S2 be non empty full SubRelStr of T2;
assume
A1: the RelStr of T1 = the RelStr of T2;
the RelStr of S2 = the RelStr of S2;
then reconsider R = S2 as full SubRelStr of T1 by A1,Th12;
assume
A2: the carrier of S1 = the carrier of S2;
then
A3: the RelStr of S1 = the RelStr of R by YELLOW_0:57;
assume
A4: for X being directed Subset of S1 st X <> {} & ex_sup_of X,T1
holds "\/"(X,T1) in the carrier of S1;
let X be directed Subset of S2 such that
A5: X <> {};
reconsider Y = X as directed Subset of S1 by A3,WAYBEL_0:3;
assume
A6: ex_sup_of X,T2;
then "\/"(Y,T1) in the carrier of S1 by A1,A4,A5,YELLOW_0:14;
hence thesis by A1,A2,A6,YELLOW_0:26;
end;
theorem
for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2
st the RelStr of T1 = the RelStr of T2 &
the carrier of S1 = the carrier of S2
holds S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting
proof
let T1,T2 be non empty RelStr;
let S1 be non empty full SubRelStr of T1;
let S2 be non empty full SubRelStr of T2;
assume
A1: the RelStr of T1 = the RelStr of T2;
the RelStr of S2 = the RelStr of S2;
then reconsider R = S2 as full SubRelStr of T1 by A1,Th12;
assume
A2: the carrier of S1 = the carrier of S2;
then
A3: the RelStr of S1 = the RelStr of R by YELLOW_0:57;
assume
A4: for X being filtered Subset of S1 st X <> {} & ex_inf_of X,T1
holds "/\"(X,T1) in the carrier of S1;
let X be filtered Subset of S2 such that
A5: X <> {};
reconsider Y = X as filtered Subset of S1 by A3,WAYBEL_0:4;
assume
A6: ex_inf_of X,T2;
then "/\"(Y,T1) in the carrier of S1 by A1,A4,A5,YELLOW_0:14;
hence thesis by A1,A2,A6,YELLOW_0:27;
end;
begin :: Nets and limits
theorem Th24:
for S,T being non empty TopSpace, N being net of S
for f being Function of S,T st f is continuous holds f.:Lim N c= Lim (f*N)
proof
let S,T be non empty TopSpace, N be net of S;
A1: [#]T <> {};
let f be Function of S,T such that
A2: f is continuous;
let p be object;
assume
A3: p in f.:Lim N;
then reconsider p as Point of T;
consider x being object such that
A4: x in the carrier of S and
A5: x in Lim N and
A6: p = f.x by A3,FUNCT_2:64;
reconsider x as Element of S by A4;
now
let V be a_neighborhood of p;
A7: p in Int V by CONNSP_2:def 1;
A8: x in f"Int V by A6,A7,FUNCT_2:38;
f"Int V is open by A1,A2,TOPS_2:43;
then f"Int V is a_neighborhood of x by A8,CONNSP_2:3;
then N is_eventually_in f"Int V by A5,YELLOW_6:def 15;
then consider i being Element of N such that
A9: for j being Element of N st j >= i holds N.j in
f"Int V;
A10: the mapping of f*N = f*the mapping of N by WAYBEL_9:def 8;
A11: the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
then reconsider i9 = i as Element of f*N;
thus f*N is_eventually_in V
proof
take i9;
let j9 be Element of f*N;
reconsider j = j9 as Element of N by A11;
A12: f.(N.j) = (f*N).j9 by A10,FUNCT_2:15;
assume j9 >= i9;
then N.j in f"Int V by A9,A11,YELLOW_0:1;
then
A13: f.(N.j) in Int V by FUNCT_2:38;
Int V c= V by TOPS_1:16;
hence thesis by A12,A13;
end;
end;
hence thesis by YELLOW_6:def 15;
end;
definition
let T be non empty RelStr;
let N be non empty NetStr over T;
redefine attr N is antitone means :: redefines antitone (WAYBEL_0, definition)
:
Def2: for i,j being Element of N st i <= j holds N.i >= N.j;
compatibility
proof
hereby
assume N is antitone;
then
A1: netmap(N,T) is antitone;
let i,j be Element of N;
assume i <= j;
hence N.i >= N.j by A1;
end;
assume
A2: for i,j being Element of N st i <= j holds N.i >= N.j;
let i,j be Element of N;
A3: N.i = netmap(N,T).i;
N.j = netmap(N,T).j;
hence thesis by A2,A3;
end;
end;
registration
let T be non empty reflexive RelStr;
let x be Element of T;
cluster {x} opp+id -> transitive directed monotone antitone;
coherence
proof
set N = {x} opp+id;
A1: the carrier of N = {x} by YELLOW_9:7;
thus N is transitive
proof
let i,j,k be Element of N;
i = x by A1,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
thus N is directed
proof
let i,j be Element of N;
A2: i = x by A1,TARSKI:def 1;
A3: i <= i;
j <= i by A1,A2,TARSKI:def 1;
hence thesis by A3;
end;
thus N is monotone
proof
let i,j be Element of N;
A4: i = x by A1,TARSKI:def 1;
j = x by A1,TARSKI:def 1;
hence thesis by A4,YELLOW_0:def 1;
end;
let i,j be Element of N;
A5: i = x by A1,TARSKI:def 1;
j = x by A1,TARSKI:def 1;
hence thesis by A5,YELLOW_0:def 1;
end;
end;
registration
let T be non empty reflexive RelStr;
cluster monotone antitone reflexive strict for net of T;
existence
proof set x = the Element of T;
take {x} opp+id;
thus thesis;
end;
end;
registration
let T be non empty RelStr;
let F be non empty Subset of T;
cluster F opp+id -> antitone;
coherence
proof
let i,j be Element of F opp+id;
A1: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
then reconsider x = i, y = j as Element of T opp by YELLOW_0:58;
assume i <= j;
then x <= y by A1,YELLOW_0:59;
then ~x >= ~y by YELLOW_7:1;
then (F opp+id).i >= ~y by YELLOW_9:7;
hence thesis by YELLOW_9:7;
end;
end;
registration
let S,T be non empty reflexive RelStr;
let f be monotone Function of S,T;
let N be antitone non empty NetStr over S;
cluster f*N -> antitone;
coherence
proof
let i,j be Element of f*N;
A1: the mapping of f*N = f*the mapping of N by WAYBEL_9:def 8;
A2: the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
then reconsider x = i, y = j as Element of N;
assume i <= j;
then x <= y by A2,YELLOW_0:1;
then N.x >= N.y by Def2;
then f.(N.x) >= f.(N.y) by WAYBEL_1:def 2;
then (f*N).i >= f.(N.y) by A1,FUNCT_2:15;
hence thesis by A1,FUNCT_2:15;
end;
end;
theorem Th25:
for S being complete LATTICE, N be net of S holds
the set of all "/\"({N.i where i is Element of N:i >= j},S)
where j is Element of N
is directed non empty Subset of S
proof
let S be complete LATTICE, N be net of S;
set X = the set of all "/\"({N.i where i is Element of N:i >= j},S)
where j is Element of N;
X c= the carrier of S
proof
let x be object;
assume x in X;
then ex j being Element of N st
x = "/\"({N.i where i is Element of N:i >= j},S);
hence thesis;
end;
then reconsider X as Subset of S;
X is non empty directed by WAYBEL11:30;
hence thesis;
end;
theorem
for S being non empty Poset, N be monotone reflexive net of S holds
the set of all "/\"({N.i where i is Element of N: i >= j}, S)
where j is Element of N
is directed non empty Subset of S
proof
let S be non empty Poset, N be monotone reflexive net of S;
set X = the set of all "/\"({N.i where i is Element of N: i >= j}, S)
where j is Element of N;
set jj = the Element of N;
A1: "/\"({N.i where i is Element of N: i >= jj}, S) in X;
X c= the carrier of S
proof
let x be object;
assume x in X;
then ex j being Element of N st
x = "/\"({N.i where i is Element of N: i >= j}, S);
hence thesis;
end;
then reconsider X as non empty Subset of S by A1;
X is directed
proof
let x,y be Element of S;
assume x in X;
then consider j1 being Element of N such that
A2: x = "/\"({N.i where i is Element of N: i >= j1}, S);
assume y in X;
then consider j2 being Element of N such that
A3: y = "/\"({N.i where i is Element of N: i >= j2}, S);
reconsider j1,j2 as Element of N;
[#]N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#]N and
A4: j >= j1 and
A5: j >= j2;
set z = "/\"({N.i where i is Element of N: i >= j}, S);
take z;
thus z in X;
deffunc up(Element of N) = {N.i where i is Element of N: i >= $1};
A6: for j being Element of N holds ex_inf_of up(j), S
proof
let j be Element of N;
reconsider j9 = j as Element of N;
now
take x = N.j;
j9 <= j9;
then
A7: x in up(j);
thus x is_<=_than up(j)
proof
let y be Element of S;
assume y in up(j);
then ex i being Element of N st y = N.i & i >= j;
hence x <= y by WAYBEL11:def 9;
end;
let y be Element of S;
assume y is_<=_than up(j);
hence y <= x by A7;
end;
hence thesis by YELLOW_0:16;
end;
then
A8: ex_inf_of up(j1), S;
A9: ex_inf_of up(j2), S by A6;
A10: ex_inf_of up(j), S by A6;
set A = {N.i where i is Element of N:i >= j};
A c= {N.k where k is Element of N:k >= j1}
proof
let a be object;
assume a in A;
then consider k being Element of N such that
A11: a = N.k and
A12: k >= j;
reconsider k as Element of N;
k >= j1 by A4,A12,ORDERS_2:3;
hence thesis by A11;
end;
hence z >= x by A2,A8,A10,YELLOW_0:35;
A c= {N.k where k is Element of N:k >= j2}
proof
let a be object;
assume a in A;
then consider k being Element of N such that
A13: a = N.k and
A14: k >= j;
reconsider k as Element of N;
k >= j2 by A5,A14,ORDERS_2:3;
hence thesis by A13;
end;
hence thesis by A3,A9,A10,YELLOW_0:35;
end;
hence thesis;
end;
theorem Th27:
for S being non empty 1-sorted, N being non empty NetStr over S, X being set
st rng the mapping of N c= X holds N is_eventually_in X
proof
let S be non empty 1-sorted, N be non empty NetStr over S;
let X be set such that
A1: rng the mapping of N c= X;
set i = the Element of N;
take i;
let j be Element of N;
N.j in rng the mapping of N by FUNCT_2:4;
hence thesis by A1;
end;
theorem Th28:
for R being /\-complete non empty Poset
for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F
proof
let R be /\-complete non empty Poset;
let F be non empty filtered Subset of R;
set N = F opp+id;
defpred P[set] means not contradiction;
deffunc F(Element of N) = inf F;
deffunc G(Element of N) = "/\"({N.i where i is Element of N: i >= $1}, R);
A1: for v being Element of N st P[v] holds F(v) = G(v)
proof
let v be Element of N;
set X = {N.i where i is Element of N: i >= v};
A2: the carrier of N = F by YELLOW_9:7;
then v in F;
then reconsider j = v as Element of R;
reconsider vv = v as Element of N;
A3: X c= F
proof
let x be object;
assume x in X;
then consider i being Element of N such that
A4: x = N.i and i >= v;
reconsider i as Element of N;
x = i by A4,YELLOW_9:7;
hence thesis by A2;
end;
vv <= vv;
then N.v in X;
then reconsider X as non empty Subset of R by A3,XBOOLE_1:1;
A5: ex_inf_of F, R by WAYBEL_0:76;
A6: ex_inf_of X, R by WAYBEL_0:76;
then
A7: inf X >= inf F by A3,A5,YELLOW_0:35;
F is_>=_than inf X
proof
let a be Element of R;
assume a in F;
then consider b being Element of R such that
A8: b in F and
A9: a >= b and
A10: j >= b by A2,WAYBEL_0:def 2;
reconsider k = b as Element of N by A8,YELLOW_9:7;
A11: N is full SubRelStr of R opp by YELLOW_9:7;
A12: j~ <= b~ by A10,LATTICE3:9;
A13: N.k = b by YELLOW_9:7;
k >= vv by A11,A12,YELLOW_0:60;
then b in X by A13;
then
A14: {b} c= X by ZFMISC_1:31;
A15: ex_inf_of {b}, R by YELLOW_0:38;
inf {b} = b by YELLOW_0:39;
then b >= inf X by A6,A14,A15,YELLOW_0:35;
hence thesis by A9,YELLOW_0:def 2;
end;
then inf F >= "/\"(X, R) by A5,YELLOW_0:31;
hence thesis by A7,ORDERS_2:2;
end;
A16: {F(j) where j is Element of N: P[j]}
= {G(k) where k is Element of N: P[k]} from FRAENKEL:sch 6(A1);
A17: ex j being Element of N st P[j];
{inf F where j is Element of N: P[j]} = {inf F} from LATTICE3:sch 1(
A17);
hence lim_inf N = "\/"({inf F}, R) by A16,WAYBEL11:def 6
.= inf F by YELLOW_0:39;
end;
theorem Th29:
for S,T being /\-complete non empty Poset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
holds lim_inf (f*(X opp+id)) = inf (f.:X)
proof
let S,T be /\-complete non empty Poset;
let X be non empty filtered Subset of S;
let f be monotone Function of S,T;
set M = X opp+id, N = f*M;
deffunc up(Element of N) = {N.i where i is Element of N: i >= $1};
deffunc infy(Element of N) = "/\"(up($1), T);
A1: the RelStr of N = the RelStr of M by WAYBEL_9:def 8;
A2: the mapping of N = f*the mapping of M by WAYBEL_9:def 8;
A3: the carrier of M = X by YELLOW_9:7;
A4: the mapping of M = id X by WAYBEL19:27;
defpred P[set] means not contradiction;
deffunc G(set) = inf (f.:X);
A5: for j being Element of N st P[j] holds infy(j) = G(j)
proof
let j be Element of N;
reconsider j as Element of N;
A6: [#]N is directed by WAYBEL_0:def 6;
then consider i9 being Element of N such that
i9 in [#]N and
A7: i9 >= j and i9 >= j;
A8: up(j) c= f.:X
proof
let a be object;
assume a in up(j);
then consider i being Element of N such that
A9: a = N.i and i >= j;
reconsider i as Element of N;
reconsider i9 = i as Element of M by A1;
A10: N.i = f.((id X).i) by A1,A2,A4,FUNCT_2:15
.= f.i9 by A3;
i9 in X by A3;
hence thesis by A9,A10,FUNCT_2:35;
end;
then
A11: up(j) c= the carrier of T by XBOOLE_1:1;
N.i9 in up(j) by A7;
then
A12: ex_inf_of up(j), T by A11,WAYBEL_0:76;
A13: ex_inf_of f.:X, T by WAYBEL_0:76;
then
A14: infy(j) >= inf (f.:X) by A8,A12,YELLOW_0:35;
infy(j) is_<=_than f.:X
proof
let x be Element of T;
assume x in f.:X;
then consider y being object such that
A15: y in the carrier of S and
A16: y in X and
A17: x = f.y by FUNCT_2:64;
reconsider y as Element of N by A1,A16,YELLOW_9:7;
consider i being Element of N such that
i in [#]N and
A18: i >= y and
A19: i >= j by A6;
i in X by A1,A3;
then reconsider xi = i, xy = y as Element of S by A15;
M is full SubRelStr of S opp by YELLOW_9:7;
then N is full SubRelStr of S opp by A1,Th12;
then xi~ >= xy~ by A18,YELLOW_0:59;
then xi <= xy by LATTICE3:9;
then
A20: f.xi <= x by A17,WAYBEL_1:def 2;
N.i = f.((id X).i) by A1,A2,A4,FUNCT_2:15
.= f.xi by A1,A3;
then f.xi in up(j) by A19;
then f.xi >= infy(j) by A12,YELLOW_4:2;
hence thesis by A20,ORDERS_2:3;
end;
then infy(j) <= inf (f.:X) by A13,YELLOW_0:31;
hence thesis by A14,ORDERS_2:2;
end;
A21: ex j being Element of N st P[j];
{infy(j) where j is Element of N: P[j]} =
{G(j) where j is Element of N: P[j]} from FRAENKEL:sch 6(A5)
.= {inf (f.:X) where j is Element of N: P[j]}
.= {inf (f.:X)} from LATTICE3:sch 1(A21);
hence lim_inf N = sup {inf (f.:X)} by WAYBEL11:def 6
.= inf (f.:X) by YELLOW_0:39;
end;
theorem Th30:
for S,T being non empty TopPoset for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f.:X
holds f*(X opp+id) is subnet of Y opp+id
proof
let S,T be non empty TopPoset;
let X be non empty filtered Subset of S;
let f be monotone Function of S,T;
let Y be non empty filtered Subset of T such that
A1: Y = f.:X;
set N = f*(X opp+id), M = Y opp+id;
A2: the RelStr of N = the RelStr of X opp+id by WAYBEL_9:def 8;
A3: the mapping of N = f*the mapping of X opp+id by WAYBEL_9:def 8;
A4: the carrier of M = Y by YELLOW_9:7;
A5: the mapping of M = id Y by WAYBEL19:27;
A6: the carrier of X opp+id = X by YELLOW_9:7;
the mapping of X opp+id = id X by WAYBEL19:27;
then
A7: the mapping of N = f|X by A3,RELAT_1:65;
then
A8: rng the mapping of N = f.:X by RELAT_1:115;
dom the mapping of N = X by A2,A6,FUNCT_2:def 1;
then reconsider g = f|X as Function of N,M by A1,A2,A4,A6,A7,A8,FUNCT_2:def 1
,RELSET_1:4;
take g;
thus the mapping of N = (the mapping of M)*g by A1,A5,A7,A8,RELAT_1:53;
let m be Element of M;
consider n being object such that
A9: n in the carrier of S and
A10: n in X and
A11: m = f.n by A1,A4,FUNCT_2:64;
reconsider n as Element of N by A2,A10,YELLOW_9:7;
take n;
let p be Element of N;
p in X by A2,A6;
then reconsider n9 = n, p9 = p as Element of S by A9;
reconsider fp = f.p9 as Element of M by A1,A2,A4,A6,FUNCT_2:35;
X opp+id is SubRelStr of S opp by YELLOW_9:7;
then
A12: N is SubRelStr of S opp by A2,Th12;
A13: M is full SubRelStr of T opp by YELLOW_9:7;
assume n <= p;
then n9~ <= p9~ by A12,YELLOW_0:59;
then n9 >= p9 by LATTICE3:9;
then f.n9 >= f.p9 by WAYBEL_1:def 2;
then (f.n9)~ <= (f.p9)~ by LATTICE3:9;
then fp >= m by A11,A13,YELLOW_0:60;
hence m <= g.p by A2,A6,FUNCT_1:49;
end;
theorem
for S,T being non empty TopPoset for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f.:X
holds Lim (Y opp+id) c= Lim (f*(X opp+id))
proof
let S,T be non empty TopPoset;
let X be non empty filtered Subset of S;
let f be monotone Function of S,T;
let Y be non empty filtered Subset of T;
assume Y = f.:X;
then f*(X opp+id) is subnet of Y opp+id by Th30;
hence thesis by YELLOW_6:32;
end;
theorem Th32:
for S being non empty reflexive RelStr, D being non empty Subset of S
holds the mapping of Net-Str D = id D & the carrier of Net-Str D = D &
Net-Str D is full SubRelStr of S
proof
let S be non empty reflexive RelStr, D be non empty Subset of S;
set N = Net-Str D;
A1: dom id D = D;
rng id D = D;
then reconsider g = id D as Function of D, the carrier of S
by A1,FUNCT_2:def 1,RELSET_1:4;
(id the carrier of S)|D = id D by FUNCT_3:1;
then
A2: N = NetStr (#D, (the InternalRel of S)|_2 D, g#) by WAYBEL17:def 4;
then the InternalRel of N c= the InternalRel of S by XBOOLE_1:17;
hence thesis by A2,YELLOW_0:def 13,def 14;
end;
theorem Th33:
for S,T being up-complete non empty Poset
for f being monotone Function of S,T
for D being non empty directed Subset of S
holds lim_inf (f*Net-Str D) = sup (f.:D)
proof
let S,T be up-complete non empty Poset, f be monotone Function of S,T;
let X be non empty directed Subset of S;
set M = Net-Str X, N = f*M;
deffunc up(Element of N) = {N.i where i is Element of N: i >= $1};
deffunc infy(Element of N) = "/\"(up($1), T);
set NT = the set of all infy(j) where j is Element of N;
A1: the RelStr of N = the RelStr of M by WAYBEL_9:def 8;
A2: the mapping of N = f*the mapping of M by WAYBEL_9:def 8;
A3: the carrier of M = X by Th32;
A4: the mapping of M = id X by Th32;
A5: now
let i be Element of N;
thus N.i = f.((id X).i) by A1,A2,A4,FUNCT_2:15
.= f.i by A1,A3;
end;
A6: for i being Element of N holds infy(i) = f.i
proof
let i be Element of N;
i in X by A1,A3;
then reconsider x = i as Element of S;
A7: i <= i;
N.i = f.x by A5;
then f.x in up(i) by A7;
then
A8: for z being Element of T st z is_<=_than up(i) holds z <= f.x;
f.x is_<=_than up(i)
proof
let z be Element of T;
assume z in up(i);
then consider j being Element of N such that
A9: z = N.j and
A10: j >= i;
reconsider j as Element of N;
j in X by A1,A3;
then reconsider y = j as Element of S;
A11: M is full SubRelStr of S by Th32;
the RelStr of S = the RelStr of S;
then N is full SubRelStr of S by A1,A11,Th12;
then y >= x by A10,YELLOW_0:59;
then f.y >= f.x by WAYBEL_1:def 2;
hence thesis by A5,A9;
end;
hence thesis by A8,YELLOW_0:31;
end;
NT = f.:X
proof
thus NT c= f.:X
proof
let x be object;
assume x in NT;
then consider j being Element of N such that
A12: x = infy(j);
reconsider j as Element of N;
A13: x = f.j by A6,A12;
j in X by A1,A3;
hence thesis by A13,FUNCT_2:35;
end;
let y be object;
assume y in f.:X;
then consider x being object such that
A14: x in the carrier of S and
A15: x in X and
A16: y = f.x by FUNCT_2:64;
reconsider x as Element of S by A14;
reconsider i = x as Element of N by A1,A15,Th32;
f.x = infy(i) by A6;
hence thesis by A16;
end;
hence thesis by WAYBEL11:def 6;
end;
theorem Th34:
for S being non empty reflexive RelStr
for D being non empty directed Subset of S
for i,j being Element of Net-Str D
holds i <= j iff (Net-Str D).i <= (Net-Str D).j
proof
let S be non empty reflexive RelStr;
let D be non empty directed Subset of S;
A1: dom id D = D;
rng id D = D;
then reconsider g = id D as Function of D, the carrier of S
by A1,FUNCT_2:def 1,RELSET_1:4;
(id the carrier of S)|D = id D by FUNCT_3:1;
then Net-Str D = Net-Str (D, g) by WAYBEL17:9;
hence thesis by WAYBEL11:def 10;
end;
theorem Th35:
for T being Lawson complete TopLattice
for D being directed non empty Subset of T holds sup D in Lim Net-Str D
proof
let T be Lawson complete TopLattice;
let D be directed non empty Subset of T;
set N = Net-Str D;
A1: the mapping of N = id D by Th32;
A2: the carrier of N = D by Th32;
set K = the prebasis of T;
now
let A be Subset of T;
assume
A3: sup D in A;
A4: K c= the topology of T by TOPS_2:64;
assume A in K;
then A is open by A4,PRE_TOPC:def 2;
then A is property(S) by WAYBEL19:36;
then consider y being Element of T such that
A5: y in D and
A6: for x being Element of T st x in D & x >= y holds x in A
by A3,WAYBEL11:def 3;
reconsider i = y as Element of N by A5,Th32;
thus N is_eventually_in A
proof
take i;
let j be Element of N;
A7: j = N.j by A1,A2;
A8: y = N.i by A1,A2;
assume j >= i;
then N.j >= N.i by Th34;
hence thesis by A2,A6,A7,A8;
end;
end;
hence thesis by WAYBEL19:25;
end;
definition
let T be non empty 1-sorted;
let N be net of T, M be non empty NetStr over T such that
A1: M is subnet of N;
mode Embedding of M,N -> Function of M,N means
:
Def3: the mapping of M = (the mapping of N)*it &
for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds m <= it.p;
existence by A1,YELLOW_6:def 9;
end;
theorem Th36:
for T being non empty 1-sorted for N being net of T, M being subnet of N
for e being Embedding of M,N, i being Element of M holds M.i = N.(e.i)
proof
let T be non empty 1-sorted;
let N be net of T, M be subnet of N;
let e be Embedding of M,N, i be Element of M;
the mapping of M = (the mapping of N)*e by Def3;
hence thesis by FUNCT_2:15;
end;
theorem Th37:
for T being complete LATTICE for N being net of T, M being subnet of N
holds lim_inf N <= lim_inf M
proof
let T be complete LATTICE;
let N be net of T, M be subnet of N;
deffunc infy(net of T) = the set of all "/\" ({$1.i where i is Element of $1:
i >= j}, T) where j is Element of $1;
A1: "\/"(infy(M), T) is_>=_than infy(N)
proof
let t be Element of T;
assume t in infy(N);
then consider j being Element of N such that
A2: t = "/\"({N.i where i is Element of N: i >= j}, T);
set e = the Embedding of M,N;
reconsider j as Element of N;
consider j9 being Element of M such that
A3: for p being Element of M st j9 <= p holds j <= e.p by Def3;
set X = {N.i where i is Element of N: i >= j};
set Y = {M.i where i is Element of M: i >= j9};
A4: ex_inf_of X, T by YELLOW_0:17;
A5: ex_inf_of Y, T by YELLOW_0:17;
Y c= X
proof
let y be object;
assume y in Y;
then consider i being Element of M such that
A6: y = M.i and
A7: i >= j9;
reconsider i as Element of M;
e.i >= j by A3,A7;
then N.(e.i) in X;
hence thesis by A6,Th36;
end;
then
A8: t <= "/\"(Y, T) by A2,A4,A5,YELLOW_0:35;
"/\"(Y, T) in infy(M);
then "/\"(Y, T) <= "\/"(infy(M), T) by YELLOW_2:22;
hence thesis by A8,YELLOW_0:def 2;
end;
A9: lim_inf M = "\/"(infy(M), T) by WAYBEL11:def 6;
lim_inf N = "\/"(infy(N), T) by WAYBEL11:def 6;
hence thesis by A1,A9,YELLOW_0:32;
end;
theorem Th38:
for T being complete LATTICE for N being net of T, M being subnet of N
for e being Embedding of M, N
st for i being Element of N, j being Element of M st e.j <= i
ex j9 being Element of M st j9 >= j & N.i >= M.j9
holds lim_inf N = lim_inf M
proof
let T be complete LATTICE;
let N be net of T, M be subnet of N;
let e be Embedding of M, N such that
A1: for i being Element of N, j being Element of M st e.j <= i
ex j9 being Element of M st j9 >= j & N.i >= M.j9;
deffunc infy(net of T) = the set of all "/\" ({$1.i where i is Element of $1:
i >= j}, T) where j is Element of $1;
"\/"(infy(N), T) is_>=_than infy(M)
proof
let t be Element of T;
assume t in infy(M);
then consider j being Element of M such that
A2: t = "/\"({M.i where i is Element of M: i >= j}, T);
reconsider j as Element of M;
set j9 = e.j;
set X = {N.i where i is Element of N: i >= j9};
set Y = {M.i where i is Element of M: i >= j};
t is_<=_than X
proof
let x be Element of T;
assume x in X;
then consider i being Element of N such that
A3: x = N.i and
A4: i >= j9;
reconsider i as Element of N;
consider k being Element of M such that
A5: k >= j and
A6: N.i >= M.k by A1,A4;
M.k in Y by A5;
then M.k >= t by A2,YELLOW_2:22;
hence thesis by A3,A6,YELLOW_0:def 2;
end;
then
A7: t <= "/\"(X, T) by YELLOW_0:33;
"/\"(X, T) in infy(N);
then "/\"(X, T) <= "\/"(infy(N), T) by YELLOW_2:22;
hence t <= "\/"(infy(N), T) by A7,YELLOW_0:def 2;
end;
then "\/"(infy(N), T) >= "\/"(infy(M), T) by YELLOW_0:32;
then lim_inf N >= "\/"(infy(M), T) by WAYBEL11:def 6;
then
A8: lim_inf N >= lim_inf M by WAYBEL11:def 6;
lim_inf M >= lim_inf N by Th37;
hence thesis by A8,YELLOW_0:def 3;
end;
theorem
for T being non empty RelStr
for N being net of T, M being non empty full SubNetStr of N
st for i being Element of N
ex j being Element of N st j >= i & j in the carrier of M
holds M is subnet of N & incl(M,N) is Embedding of M,N
proof
let T be non empty RelStr;
let N be net of T, M be non empty full SubNetStr of N such that
A1: for i being Element of N
ex j being Element of N st j >= i & j in the carrier of M;
A2: the mapping of M = (the mapping of N)|the carrier of M by YELLOW_6:def 6;
A3: M is full SubRelStr of N by YELLOW_6:def 7;
then
A4: the carrier of M c= the carrier of N by YELLOW_0:def 13;
M is directed
proof
let x,y be Element of M;
reconsider i = x, j = y as Element of N by A3,YELLOW_0:58;
consider k being Element of N such that
A5: k >= i and
A6: k >= j by YELLOW_6:def 3;
consider l being Element of N such that
A7: l >= k and
A8: l in the carrier of M by A1;
reconsider z = l as Element of M by A8;
take z;
A9: l >= i by A5,A7,YELLOW_0:def 2;
l >= j by A6,A7,YELLOW_0:def 2;
hence thesis by A9,YELLOW_6:12;
end;
then reconsider K = M as net of T by A3;
A10: now
set f = incl(K,N);
A11: f = id the carrier of K by A4,YELLOW_9:def 1;
hence the mapping of K = (the mapping of N)*f by A2,RELAT_1:65;
let m be Element of N;
consider j being Element of N such that
A12: j >= m and
A13: j in the carrier of K by A1;
reconsider n = j as Element of K by A13;
take n;
let p be Element of K;
reconsider q = p as Element of N by A3,YELLOW_0:58;
assume n <= p;
then
A14: j <= q by YELLOW_6:11;
f.p = q by A11;
hence m <= f.p by A12,A14,YELLOW_0:def 2;
end;
hence M is subnet of N by YELLOW_6:def 9;
hence thesis by A10,Def3;
end;
theorem Th40:
for T being non empty RelStr, N being net of T for i being Element of N holds
N|i is subnet of N & incl(N|i,N) is Embedding of N|i, N
proof
let T be non empty RelStr, N be net of T;
let i be Element of N;
set M = N|i, f = incl(M,N);
thus N|i is subnet of N;
thus N|i is subnet of N;
N|i is full SubNetStr of N by WAYBEL_9:14;
then
A1: N|i is full SubRelStr of N by YELLOW_6:def 7;
A2: incl(N|i,N) = id the carrier of N|i by WAYBEL_9:13,YELLOW_9:def 1;
the mapping of M = (the mapping of N)|the carrier of M by WAYBEL_9:def 7;
hence the mapping of M = (the mapping of N)*f by A2,RELAT_1:65;
let m be Element of N;
consider n9 being Element of N such that
A3: n9 >= i and
A4: n9 >= m by YELLOW_6:def 3;
reconsider n = n9 as Element of M by A3,WAYBEL_9:def 7;
take n;
let p be Element of M;
reconsider p9 = p as Element of N by A1,YELLOW_0:58;
assume n <= p;
then n9 <= p9 by A1,YELLOW_0:59;
then m <= p9 by A4,YELLOW_0:def 2;
hence thesis by A2;
end;
theorem Th41:
for T being complete LATTICE, N being net of T
for i being Element of N holds lim_inf (N|i) = lim_inf N
proof
let T be complete LATTICE, N be net of T;
let i be Element of N;
reconsider M = N|i as subnet of N;
reconsider e = incl(M,N) as Embedding of M, N by Th40;
M is full SubNetStr of N by WAYBEL_9:14;
then
A1: M is full SubRelStr of N by YELLOW_6:def 7;
A2: incl(M,N) = id the carrier of M by WAYBEL_9:13,YELLOW_9:def 1;
now
let k be Element of N, j be Element of M;
consider j9 being Element of N such that
A3: j9 = j and
A4: j9 >= i by WAYBEL_9:def 7;
assume e.j <= k;
then
A5: k >= j9 by A2,A3;
then k >= i by A4,YELLOW_0:def 2;
then reconsider k9 = k as Element of M by WAYBEL_9:def 7;
take k9;
thus k9 >= j by A1,A3,A5,YELLOW_0:60;
A6: M.k9 = N.(e.k9) by Th36;
M.k9 <= M.k9;
hence N.k >= M.k9 by A2,A6;
end;
hence thesis by Th38;
end;
theorem Th42:
for T being non empty RelStr, N being net of T, X being set
st N is_eventually_in X
ex i be Element of N st N.i in X & rng the mapping of N|i c= X
proof
let T be non empty RelStr, N be net of T, X be set;
given i9 being Element of N such that
A1: for j being Element of N st j >= i9 holds N.j in X;
[#]N is directed by WAYBEL_0:def 6;
then consider i being Element of N such that
i in [#]N and
A2: i9 <= i and i9 <= i;
take i;
thus N.i in X by A1,A2;
let x be object;
assume x in rng the mapping of N|i;
then consider j being object such that
A3: j in dom the mapping of N|i and
A4: x = (the mapping of N|i).j by FUNCT_1:def 3;
A5: dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1;
reconsider j as Element of N|i by A3;
the carrier of N|i = {y where y is Element of N: i <= y} by WAYBEL_9:12;
then consider k being Element of N such that
A6: j = k and
A7: i <= k by A3,A5;
x = (N|i).j by A4
.= N.k by A6,WAYBEL_9:16;
hence thesis by A1,A2,A7,ORDERS_2:3;
end;
theorem Th43: :: see WAYBEL_2:18, for eventually-directed
for T being Lawson complete TopLattice
for N being eventually-filtered net of T
holds rng the mapping of N is filtered non empty Subset of T
proof
let T be Lawson complete TopLattice;
let N be eventually-filtered net of T;
reconsider F = rng the mapping of N as non empty Subset of T;
F is filtered
proof
let x,y be Element of T;
assume x in F;
then consider i1 being object such that
A1: i1 in dom the mapping of N and
A2: x = (the mapping of N).i1 by FUNCT_1:def 3;
assume y in F;
then consider i2 being object such that
A3: i2 in dom the mapping of N and
A4: y = (the mapping of N).i2 by FUNCT_1:def 3;
A5: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
reconsider i1, i2 as Element of N by A1,A3;
consider j1 being Element of N such that
A6: for k being Element of N st j1 <= k holds N.i1 >= N.k by WAYBEL_0:12;
consider j2 being Element of N such that
A7: for k being Element of N st j2 <= k holds N.i2 >= N.k by WAYBEL_0:12;
consider j being Element of N such that
A8: j2 <= j and
A9: j1 <= j by YELLOW_6:def 3;
take z = N.j;
thus z in F by A5,FUNCT_1:def 3;
thus thesis by A2,A4,A6,A7,A8,A9;
end;
hence thesis;
end;
theorem Th44:
:: 1.7. LEMMA, -- WAYBEL19:44 revised
for T being Lawson complete TopLattice
for N being eventually-filtered net of T holds Lim N = {inf N}
proof
let T be Lawson complete TopLattice;
set S = the Scott TopAugmentation of T;
let N be eventually-filtered net of T;
reconsider F = rng the mapping of N
as filtered non empty Subset of T by Th43;
A1: the topology of S = sigma T by YELLOW_9:51;
A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
A3: inf N = Inf the mapping of N by WAYBEL_9:def 2
.= "/\"(F, T) by YELLOW_2:def 6;
A4: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
thus Lim N c= {inf N}
proof
let p be object;
assume
A5: p in Lim N;
then reconsider p as Element of T;
p is_<=_than F
proof
let u be Element of T;
assume u in F;
then consider i being object such that
A6: i in dom the mapping of N and
A7: u = (the mapping of N).i by FUNCT_1:def 3;
reconsider i as Element of N by A6;
consider ii being Element of N such that
A8: for k being Element of N st ii <= k holds N.i >= N.k by WAYBEL_0:12;
downarrow u is closed by WAYBEL19:38;
then
A9: Cl downarrow u = downarrow u by PRE_TOPC:22;
N is_eventually_in downarrow u
proof
take ii;
let j be Element of N;
assume j >= ii;
then N.j <= N.i by A8;
hence thesis by A7,WAYBEL_0:17;
end;
then Lim N c= downarrow u by A9,WAYBEL19:26;
hence thesis by A5,WAYBEL_0:17;
end;
then
A10: p <= inf N by A3,YELLOW_0:33;
inf N is_<=_than F by A3,YELLOW_0:33;
then
A11: F c= uparrow inf N by YELLOW_2:2;
uparrow inf N is closed by WAYBEL19:38;
then Cl uparrow inf N = uparrow inf N by PRE_TOPC:22;
then
A12: Cl F c= uparrow inf N by A11,PRE_TOPC:19;
p in Cl F by A5,WAYBEL_9:24;
then p >= inf N by A12,WAYBEL_0:18;
then p = inf N by A10,ORDERS_2:2;
hence thesis by TARSKI:def 1;
end;
reconsider K = (sigma T) \/
the set of all (uparrow x)` where x is Element of T as prebasis of T
by WAYBEL19:30;
now
let A be Subset of T;
assume that
A13: inf F in A and
A14: A in K;
per cases by A14,XBOOLE_0:def 3;
suppose
A15: A in sigma T;
then reconsider a = A as Subset of S by A1;
a is open by A1,A15,PRE_TOPC:def 2;
then a is upper by WAYBEL11:def 4;
then
A16: A is upper by A2,WAYBEL_0:25;
set i = the Element of N;
thus N is_eventually_in A
proof
take i;
let j be Element of N;
N.j in F by A4,FUNCT_1:def 3;
then N.j >= inf F by YELLOW_2:22;
hence thesis by A13,A16;
end;
end;
suppose
A in the set of all (uparrow x)` where x is Element of T;
then consider x being Element of T such that
A17: A = (uparrow x)`;
not inf F >= x by A13,A17,YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A18: y in F and
A19: not y >= x;
consider i being object such that
A20: i in the carrier of N and
A21: y = (the mapping of N).i by A4,A18,FUNCT_1:def 3;
thus N is_eventually_in A
proof
reconsider i as Element of N by A20;
consider ii being Element of N such that
A22: for k being Element of N st ii <= k holds N.i >= N.k by WAYBEL_0:12;
take ii;
let j be Element of N;
assume j >= ii;
then N.j <= N.i by A22;
then not N.j >= x by A19,A21,ORDERS_2:3;
hence thesis by A17,YELLOW_9:1;
end;
end;
end;
then inf F in Lim N by WAYBEL19:25;
hence thesis by A3,ZFMISC_1:31;
end;
begin :: Lawson topology revisited
theorem Th45:
:: 1.8. THEOREM, (1) <=> (2), generalized, p. 145
for S,T being Lawson complete TopLattice
for f being meet-preserving Function of S,T holds
f is continuous iff f is directed-sups-preserving &
for X being non empty Subset of S holds f preserves_inf_of X
proof
let S,T be Lawson complete TopLattice;
A1: [#]T <> {};
set Ss = the Scott TopAugmentation of S,Ts = the Scott TopAugmentation of T,Sl
= the lower correct TopAugmentation of S,Tl = the lower correct TopAugmentation
of T;
A2: S is TopAugmentation of S by YELLOW_9:44;
A3: T is TopAugmentation of T by YELLOW_9:44;
A4: S is Refinement of Ss,Sl by A2,WAYBEL19:29;
A5: T is Refinement of Ts,Tl by A3,WAYBEL19:29;
A6: T is TopAugmentation of Ts by YELLOW_9:45;
A7: S is TopAugmentation of Ss by YELLOW_9:45;
A8: the RelStr of Ss = the RelStr of S by YELLOW_9:def 4;
A9: the RelStr of Sl = the RelStr of S by YELLOW_9:def 4;
A10: the RelStr of Ts = the RelStr of T by YELLOW_9:def 4;
A11: the RelStr of Tl = the RelStr of T by YELLOW_9:def 4;
let f be meet-preserving Function of S,T;
reconsider g = f as Function of Sl,Tl by A9,A11;
reconsider h = f as Function of Ss,Ts by A8,A10;
A12: [#]Ts <> {};
hereby
assume
A13: f is continuous;
now
let P be Subset of Ts;
reconsider A = P as Subset of Ts;
reconsider C = A as Subset of T by A10;
assume
A14: P is open;
then C is open by A6,WAYBEL19:37;
then
A15: f"C is open by A1,A13,TOPS_2:43;
A is upper by A14,WAYBEL11:def 4;
then h"A is upper by A8,A10,WAYBEL17:2,WAYBEL_9:1;
then f"C is upper by A8,WAYBEL_0:25;
hence h"P is open by A7,A15,WAYBEL19:41;
end;
then h is continuous by A12,TOPS_2:43;
hence f is directed-sups-preserving by A8,A10,Th6;
for X being non empty filtered Subset of S holds f preserves_inf_of X
proof
let F be non empty filtered Subset of S;
assume ex_inf_of F,S;
thus ex_inf_of f.:F,T by YELLOW_0:17;
{inf F} = Lim (F opp+id) by WAYBEL19:43;
then Im(f,inf F) c= Lim (f*(F opp+id)) by A13,Th24;
then {f.inf F} c= Lim (f*(F opp+id)) by SETWISEO:8;
then
A16: f.inf F in Lim (f*(F opp+id)) by ZFMISC_1:31;
reconsider G = f.:F as filtered non empty Subset of T by WAYBEL20:24;
A17: rng the mapping of f*(F opp+id)
= rng (f*the mapping of F opp+id) by WAYBEL_9:def 8
.= rng (f * id F) by WAYBEL19:27
.= rng (f|F) by RELAT_1:65
.= G by RELAT_1:115;
Lim (f*(F opp+id)) = {inf (f*(F opp+id))} by Th44
.= {Inf the mapping of f*(F opp+id)} by WAYBEL_9:def 2
.= {inf G} by A17,YELLOW_2:def 6;
hence thesis by A16,TARSKI:def 1;
end;
hence for X being non empty Subset of S holds f preserves_inf_of X by Th4;
end;
assume f is directed-sups-preserving;
then
A18: h is directed-sups-preserving by A8,A10,Th6;
assume for X being non empty Subset of S holds f preserves_inf_of X;
then for X being non empty Subset of Sl
holds g preserves_inf_of X by A9,A11,WAYBEL_0:65;
then g is continuous by WAYBEL19:8;
hence thesis by A4,A5,A18,WAYBEL19:24;
end;
theorem Th46:
:: 1.8. THEOREM, (1) <=> (2), p. 145
for S,T being Lawson complete TopLattice
for f being SemilatticeHomomorphism of S,T holds
f is continuous iff f is infs-preserving directed-sups-preserving
proof
let S,T be Lawson complete TopLattice;
let f be SemilatticeHomomorphism of S,T;
hereby
assume
A1: f is continuous;
A2: for X being finite Subset of S holds f preserves_inf_of X by Def1;
for X being non empty filtered Subset of S holds f preserves_inf_of X
by A1,Th45;
hence f is infs-preserving by A2,WAYBEL_0:71;
thus f is directed-sups-preserving by A1,Th45;
end;
assume f is infs-preserving;
then for X being non empty Subset of S holds f preserves_inf_of X;
hence thesis by Th45;
end;
definition
let S,T be non empty RelStr;
let f be Function of S,T;
attr f is lim_infs-preserving means
for N being net of S holds f.lim_inf N = lim_inf (f*N);
end;
theorem
:: 1.8. THEOREM, (1) <=> (3), p. 145
for S,T being Lawson complete TopLattice
for f being SemilatticeHomomorphism of S,T holds
f is continuous iff f is lim_infs-preserving
proof
let S,T be Lawson complete TopLattice;
let f be SemilatticeHomomorphism of S,T;
thus f is continuous implies f is lim_infs-preserving
proof
assume f is continuous;
then
A1: f is infs-preserving directed-sups-preserving by Th46;
let N be net of S;
set M = f*N;
set Y = the set of all "/\"({M.i where i is Element of M:i >= j},T)
where j is Element of M;
reconsider X = the set of all "/\" ({N.i where i is Element of N:i >= j},S)
where j is Element of N
as directed non empty Subset of S by Th25;
A2: ex_sup_of X,S by YELLOW_0:17;
A3: f preserves_sup_of X by A1;
A4: the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
A5: the carrier of S c= dom f by FUNCT_2:def 1;
deffunc A(Element of N) = {N.i where i is Element of N: i >= $1};
deffunc INF(Element of N) = "/\"(A($1),S);
defpred P[set] means not contradiction;
A6: f.:{INF(i) where i is Element of N: P[i]}
= {f.INF(i) where i is Element of N: P[i]} from LATTICE3:sch 2(A5);
A7: f.:X = Y
proof
A8: now
let j be Element of N;
let j9 be Element of M such that
A9: j9 = j;
defpred Q[Element of N] means $1 >= j;
defpred Q9[Element of M] means $1 >= j9;
deffunc F(Element of N) = f.(N.$1);
deffunc G(set) = f.((the mapping of N).$1);
A10: for v being Element of N st Q[v] holds F(v) = G(v);
deffunc H(set) = (f*the mapping of N).$1;
deffunc I(Element of M) = M.$1;
A11: for v being Element of N st Q[v] holds G(v) = H(v) by FUNCT_2:15;
A12: for v being Element of M st Q9[v] holds H(v) = I(v) by WAYBEL_9:def 8;
defpred P[set] means [j9,$1] in the InternalRel of N;
A13: for v being Element of N holds Q[v] iff P[v] by A9,ORDERS_2:def 5;
A14: for v being Element of M holds P[v] iff Q9[v] by A4,ORDERS_2:def 5;
deffunc N(Element of N) = N.$1;
thus f.:A(j) = f.:{N(i) where i is Element of N: Q[i]}
.= {f.(N(k)) where k is Element of N: Q[k]} from LATTICE3:sch 2(A5)
.= {F(k) where k is Element of N: Q[k]}
.= {G(s) where s is Element of N: Q[s]} from FRAENKEL:sch 6(A10)
.= {H(o) where o is Element of N: Q[o]} from FRAENKEL:sch 6(A11)
.= {H(r) where r is Element of N: P[r]} from FRAENKEL:sch 3(A13)
.= {H(m) where m is Element of M: P[m]} by A4
.= {H(q) where q is Element of M: Q9[q]} from FRAENKEL:sch 3(A14)
.= {I(n) where n is Element of M: Q9[n]} from FRAENKEL:sch 6(A12)
.= {M.n where n is Element of M: n >= j9};
end;
A15: now
let j be Element of N;
A(j) c= the carrier of S
proof
let b be object;
assume b in A(j);
then ex i being Element of N st b = N.i & i >= j;
hence thesis;
end;
then reconsider A = A(j) as Subset of S;
A16: f preserves_inf_of A by A1;
ex_inf_of A,S by YELLOW_0:17;
hence f."/\"(A(j),S) = "/\"(f.:A(j), T) by A16;
end;
thus f.:X c= Y
proof
let a be object;
assume a in f.:X;
then consider j being Element of N such that
A17: a = f."/\" ({N.i where i is Element of N:i >= j},S) by A6;
A18: a = "/\"(f.:A(j),T) by A15,A17;
reconsider j9 = j as Element of M by A4;
f.:A(j) = {M.n where n is Element of M: n >= j9} by A8;
hence thesis by A18;
end;
let a be object;
assume a in Y;
then consider j9 being Element of M such that
A19: a = "/\"({M.n where n is Element of M: n >= j9},T);
reconsider j = j9 as Element of N by A4;
a = "/\"(f.:A(j),T) by A8,A19
.= f."/\"(A(j),S) by A15;
hence thesis by A6;
end;
thus f.lim_inf N = f.sup X by WAYBEL11:def 6
.= sup (f.:X) by A2,A3
.= lim_inf (f*N) by A7,WAYBEL11:def 6;
end;
assume
A20: for N being net of S holds f.lim_inf N = lim_inf (f*N);
A21: f is directed-sups-preserving
proof
let D be Subset of S;
assume D is non empty directed;
then reconsider D9 = D as non empty directed Subset of S;
assume ex_sup_of D, S;
thus ex_sup_of f.:D, T by YELLOW_0:17;
thus f.sup D = f.lim_inf Net-Str D9 by WAYBEL17:10
.= lim_inf (f*Net-Str D9) by A20
.= sup (f.:D) by Th33;
end;
A22: for X being finite Subset of S holds f preserves_inf_of X by Def1;
now
let X be non empty filtered Subset of S;
reconsider fX = f.:X as filtered non empty Subset of T by WAYBEL20:24;
thus f preserves_inf_of X
proof
assume ex_inf_of X,S;
thus ex_inf_of f.:X,T by YELLOW_0:17;
f.inf X = f.lim_inf (X opp+id) by Th28
.= lim_inf (f*(X opp+id)) by A20
.= inf fX by Th29
.= lim_inf (fX opp+id) by Th28;
hence thesis by Th28;
end;
end;
then f is infs-preserving by A22,WAYBEL_0:71;
hence thesis by A21,Th46;
end;
theorem Th48:
:: 1.11. THEOREM, (1) => (2a), p. 147
for T being Lawson complete continuous TopLattice
for S being meet-inheriting full non empty SubRelStr of T
st Top T in the carrier of S &
ex X being Subset of T st X = the carrier of S & X is closed
holds S is infs-inheriting
proof
let T be Lawson complete continuous TopLattice;
let S be meet-inheriting full non empty SubRelStr of T such that
A1: Top T in the carrier of S;
given X being Subset of T such that
A2: X = the carrier of S and
A3: X is closed;
S is filtered-infs-inheriting
proof
let Y be filtered Subset of S;
assume Y <> {};
then reconsider F = Y as filtered non empty Subset of T by YELLOW_2:7;
set N = F opp+id;
assume ex_inf_of Y, T;
the mapping of N = id Y by WAYBEL19:27;
then
A4: rng the mapping of N = Y;
Lim N = {inf F} by WAYBEL19:43;
then {inf F} c= Cl X by A2,A4,Th27,WAYBEL19:26;
then {inf F} c= X by A3,PRE_TOPC:22;
hence thesis by A2,ZFMISC_1:31;
end;
hence thesis by A1,Th16;
end;
theorem Th49:
:: 1.11. THEOREM, (1) => (2b), p. 147
for T being Lawson complete continuous TopLattice
for S being full non empty SubRelStr of T
st ex X being Subset of T st X = the carrier of S & X is closed
holds S is directed-sups-inheriting
proof
let T be Lawson complete continuous TopLattice;
let S be full non empty SubRelStr of T;
given X being Subset of T such that
A1: X = the carrier of S and
A2: X is closed;
let Y be directed Subset of S;
assume Y <> {};
then reconsider D = Y as directed non empty Subset of T by YELLOW_2:7;
set N = Net-Str D;
assume ex_sup_of Y,T;
the mapping of N = id Y by Th32;
then rng the mapping of N = Y;
then Lim N c= Cl X by A1,Th27,WAYBEL19:26;
then
A3: Lim N c= X by A2,PRE_TOPC:22;
sup D in Lim N by Th35;
hence thesis by A1,A3;
end;
theorem Th50:
:: 1.11. THEOREM, (2) => (1), p. 147
for T being Lawson complete continuous TopLattice
for S being infs-inheriting directed-sups-inheriting full non empty
SubRelStr of T ex X being Subset of T st X = the carrier of S & X is closed
proof
let T be Lawson complete continuous TopLattice;
let S be infs-inheriting directed-sups-inheriting full non empty
SubRelStr of T;
reconsider X = the carrier of S as Subset of T by YELLOW_0:def 13;
take X;
thus X = the carrier of S;
reconsider S as complete CLSubFrame of T by Th18;
set SL = the Lawson correct TopAugmentation of S;
A1: the RelStr of SL = the RelStr of S by YELLOW_9:def 4;
set f = incl(SL,T), f9 = incl(S,T);
A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;
then
A3: f = id the carrier of SL by A1,YELLOW_9:def 1;
A4: f9 = id the carrier of SL by A1,A2,YELLOW_9:def 1;
A5: [#]SL is compact by COMPTS_1:1;
A6: f9 is infs-preserving by Th8;
the RelStr of T = the RelStr of T;
then
A7: f is infs-preserving directed-sups-preserving by A1,A3,A4,A6,Th6,Th10;
then f is SemilatticeHomomorphism of SL,T by Th5;
then f is continuous by A7,Th46;
then f.:[#]SL is compact by A5,WEIERSTR:8;
then X is compact by A1,A3,FUNCT_1:92;
hence thesis by COMPTS_1:7;
end;
theorem Th51:
:: 1.11. THEOREM, (2) => (3+), p. 147
for T being Lawson complete continuous TopLattice
for S being infs-inheriting directed-sups-inheriting full non empty
SubRelStr of T for N being net of T st N is_eventually_in the carrier of S
holds lim_inf N in the carrier of S
proof
let T be Lawson complete continuous TopLattice;
let S be infs-inheriting directed-sups-inheriting full non empty
SubRelStr of T;
set X = the carrier of S;
let N be net of T;
assume N is_eventually_in X;
then consider a being Element of N such that
N.a in X and
A1: rng the mapping of N|a c= X by Th42;
deffunc up(Element of N|a) = {N|a.i where i is Element of N|a: i >= $1};
reconsider iN = the set of all "/\"(up(j), T)
where j is Element of N|a
as directed non empty Subset of T by Th25;
iN c= X
proof
let z be object;
assume z in iN;
then consider j being Element of N|a such that
A2: z = "/\"(up(j), T);
up(j) c= X
proof
let u be object;
assume u in up(j);
then ex i being Element of N|a st ( u = (N|a).i)&( i >= j);
then u in rng the mapping of N|a by FUNCT_2:4;
hence thesis by A1;
end;
then reconsider Xj = up(j) as Subset of S;
ex_inf_of Xj, T by YELLOW_0:17;
hence thesis by A2,YELLOW_0:def 18;
end;
then reconsider jN = iN as non empty Subset of S;
A3: jN is directed by WAYBEL10:23;
ex_sup_of jN,T by YELLOW_0:17;
then "\/"(jN,T) in the carrier of S by A3,WAYBEL_0:def 4;
then lim_inf (N|a) in X by WAYBEL11:def 6;
hence thesis by Th41;
end;
theorem Th52:
:: 1.11. THEOREM, (3) => (2a), p. 147
for T being Lawson complete continuous TopLattice
for S being meet-inheriting full non empty SubRelStr of T
st Top T in the carrier of S &
for N being net of T st rng the mapping of N c= the carrier of S
holds lim_inf N in the carrier of S holds S is infs-inheriting
proof
let T be Lawson complete continuous TopLattice;
let S be meet-inheriting full non empty SubRelStr of T such that
A1: Top T in the carrier of S;
set X = the carrier of S;
assume
A2: for N being net of T st rng the mapping of N c= X holds lim_inf N in X;
S is filtered-infs-inheriting
proof
let Y be filtered Subset of S;
assume Y <> {};
then reconsider F = Y as non empty filtered Subset of T by YELLOW_2:7;
assume ex_inf_of Y,T;
the mapping of F opp+id = id F by WAYBEL19:27;
then
A3: rng the mapping of F opp+id = Y;
lim_inf (F opp+id) = inf F by Th28;
hence thesis by A2,A3;
end;
hence thesis by A1,Th16;
end;
theorem Th53:
:: 1.11. THEOREM, (3) => (2b), p. 147
for T being Lawson complete continuous TopLattice
for S being full non empty SubRelStr of T
st for N being net of T st rng the mapping of N c= the carrier of S
holds lim_inf N in the carrier of S holds S is directed-sups-inheriting
proof
let T be Lawson complete continuous TopLattice;
let S be full non empty SubRelStr of T;
set X = the carrier of S;
assume
A1: for N being net of T st rng the mapping of N c= X holds lim_inf N in X;
let Y be directed Subset of S;
assume Y <> {};
then reconsider F = Y as non empty directed Subset of T by YELLOW_2:7;
assume ex_sup_of Y,T;
the mapping of Net-Str F = id F by Th32;
then
A2: rng the mapping of Net-Str F = Y;
lim_inf Net-Str F = sup F by WAYBEL17:10;
hence thesis by A1,A2;
end;
theorem
:: 1.11. THEOREM, (1) <=> (3+), p. 147
for T being Lawson complete continuous TopLattice
for S being meet-inheriting full non empty SubRelStr of T
for X being Subset of T st X = the carrier of S & Top T in X holds
X is closed iff
for N being net of T st N is_eventually_in X holds lim_inf N in X
proof
let T be Lawson complete continuous TopLattice;
let S be meet-inheriting full non empty SubRelStr of T;
let X be Subset of T such that
A1: X = the carrier of S and
A2: Top T in X;
hereby
assume X is closed;
then S is infs-inheriting directed-sups-inheriting full non empty
SubRelStr of T by A1,A2,Th48,Th49;
hence
for N being net of T st N is_eventually_in X holds lim_inf N in X
by A1,Th51;
end;
assume for N being net of T st N is_eventually_in X holds lim_inf N in X;
then for N being net of T st rng the mapping of N c= the carrier of S
holds lim_inf N in the carrier of S by A1,Th27;
then S is infs-inheriting directed-sups-inheriting by A1,A2,Th52,Th53;
then ex X being Subset of T st X = the carrier of S & X is closed by Th50;
hence thesis by A1;
end;