Copyright (c) 1998 Association of Mizar Users
environ
vocabulary WAYBEL_0, LATTICES, PRE_TOPC, FINSET_1, FUNCOP_1, YELLOW_0, BOOLE,
RELAT_1, FUNCT_1, ORDINAL2, SEQM_3, LATTICE3, ORDERS_1, QUANTAL1, BHSP_3,
CAT_1, FUNCT_3, WELLORD1, WAYBEL_5, CONNSP_2, TOPS_1, RELAT_2, WAYBEL_9,
OPPCAT_1, SUBSET_1, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1, YELLOW_9,
PROB_1, YELLOW_2, PRELAMB, COMPTS_1, WAYBEL21;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
TOLER_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1,
ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3,
WAYBEL_5, YELLOW_6, YELLOW_7, BORSUK_1, WAYBEL_9, YELLOW_9, WAYBEL11,
WAYBEL17, WAYBEL19;
constructors TOLER_1, ORDERS_3, WAYBEL_1, CANTOR_1, TOPS_1, WAYBEL_3,
NATTRA_1, URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL17, MEMBERED, PARTFUN1;
clusters STRUCT_0, YELLOW_0, RELSET_1, LATTICE3, WAYBEL_0, FINSET_1, PUA2MSS1,
YELLOW_6, WAYBEL_2, WAYBEL_9, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL19,
SUBSET_1, MEMBERED, RELAT_1, ZFMISC_1, FUNCT_2, PARTFUN1;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_6,
XBOOLE_0;
theorems YELLOW_0, WAYBEL_0, WAYBEL_6, PRE_TOPC, FUNCOP_1, RELAT_1, BORSUK_1,
FUNCT_2, TOPS_1, TOPS_2, ZFMISC_1, CONNSP_2, WAYBEL_9, YELLOW_9, FUNCT_1,
WAYBEL_1, YELLOW_6, WAYBEL19, WELLORD1, SETWISEO, FUNCT_3, TARSKI,
CANTOR_1, LATTICE3, FINSET_1, WAYBEL11, WAYBEL17, ORDERS_1, 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 -> map 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 map of S,T;
take f; let X be finite Subset of S such that
A2: ex_inf_of X,S;
per cases; suppose X = {};
then A3: f.:X = {} & S is upper-bounded by A2,RELAT_1:149,WAYBEL20:5;
hence ex_inf_of f.:X,T by A1,YELLOW_0:43;
thus f.inf X = Top T by FUNCOP_1:13 .= inf (f.:X) by A3,YELLOW_0:def 12;
suppose X <> {};
then reconsider A = X as non empty Subset of S;
consider a being Element of A;
reconsider a as Element of S;
dom f = the carrier of S & f.a = Top T by FUNCOP_1:13,19;
then Top T in f.:X by FUNCT_1:def 12;
then {Top T} c= f.:X & f.:X c= {Top T} by BORSUK_1:6,ZFMISC_1:37;
then {Top T} = f.:X & f.inf X = Top T by FUNCOP_1:13,XBOOLE_0:def 10;
hence thesis by YELLOW_0:38,39;
end;
end;
definition
let S,T be Semilattice;
cluster meet-preserving -> monotone map of S,T;
coherence
proof let f be map 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;
definition
let S be Semilattice, T be upper-bounded Semilattice;
cluster -> meet-preserving SemilatticeHomomorphism of S,T;
coherence
proof let f be SemilatticeHomomorphism of S,T;
let x,y be Element of S; thus f preserves_inf_of {x,y} by Def1;
end;
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;
f preserves_inf_of {}S & ex_inf_of {}S,S by Def1,YELLOW_0:43;
then f.inf {}S = inf (f.:{}S) by WAYBEL_0:def 30;
hence f.Top S = inf (f.:{}S) by YELLOW_0:def 12 .= inf {}T by RELAT_1:149
.= Top T by YELLOW_0:def 12;
end;
theorem Th2:
for S,T being Semilattice, f being map 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 map 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 & x c= X & P[x];
thus P[x \/ {y}]
proof assume x \/ {y} <> {};
reconsider y' = y as Element of S by A5;
set fy = f.y';
A6: ex_inf_of {fy}, T & inf {fy} = fy &
ex_inf_of {y'}, S & inf {y'} = y by YELLOW_0:38,39;
hence ex_inf_of x \/ {y}, S by A5,YELLOW_2:4;
A7: dom f = the carrier of S by FUNCT_2:def 1;
then f.:{y} = {fy} by FUNCT_1:117;
then A8: f.:(x \/ {y}) = (f.:x) \/ {fy} by RELAT_1:153;
hence ex_inf_of f.:(x \/ {y}), T by A5,A6,A7,FUNCT_1:117,YELLOW_2:4;
per cases; suppose x = {};
hence "/\"(f.:(x \/ {y}), T) = f."/\"(x \/ {y}, S) by A6,A7,FUNCT_1:117;
suppose
A9: x <> {};
hence "/\"(f.:(x \/ {y}), T)
= (f."/\"(x, S)) "/\" fy by A5,A6,A8,YELLOW_2:4
.= f.("/\"(x, S)"/\" y') by A1,WAYBEL_6:1
.= f."/\"(x \/ {y}, S) by A5,A6,A9,YELLOW_2:4;
end;
end;
P[X] from Finite(A2,A3,A4);
hence thesis;
end;
theorem
for S,T being upper-bounded Semilattice, f being meet-preserving map 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 map 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;
f.:{} = {} & Top S = "/\"({},S) by RELAT_1:149,YELLOW_0:def 12;
then A2: ex_inf_of f.:{}, T & "/\"(f.:{}, T) = f."/\"
({}, S) by A1,YELLOW_0:43,def 12;
X = {} or f preserves_inf_of X by Th2;
hence thesis by A2,WAYBEL_0:def 30;
end;
theorem Th4:
for S,T being Semilattice, f being map 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 map 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[set] 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 set holds x in Z iff x in the carrier of S & P[x]
from Separation;
consider a being Element of X;
A5: ex_inf_of {a}, S & inf {a} = a & {a} c= X
by YELLOW_0:38,39,ZFMISC_1:37;
Z c= the carrier of S proof let x be set; thus thesis by A4; end;
then reconsider Z as non empty Subset of S by A4,A5;
A6: now let Y be finite Subset of X;
Y is Subset of S by XBOOLE_1:1;
then Y is finite Subset of S;
hence Y <> {} implies ex_inf_of Y, S by YELLOW_0:55;
end;
A7: now let Y be finite Subset of X;
Y is Subset of S by XBOOLE_1:1;
then reconsider Y' = Y as Subset of S;
assume
A8: Y <> {};
then ex_inf_of Y', S by YELLOW_0:55;
hence "/\"(Y,S) in Z by A4,A8;
end;
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 A9: Z is filtered & ex_inf_of Z, S & inf Z = inf X & Z <> {}
by A3,A6,A7,WAYBEL_0:56,58,59;
then f preserves_inf_of Z by A2;
then A10: ex_inf_of f.:Z,T & inf (f.:Z) = f.inf Z & inf Z = inf X
by A9,WAYBEL_0:def 30;
X c= Z
proof let x be set; assume
A11: x in X;
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:37;
reconsider x as Element of S by A11;
Y is Subset of S by XBOOLE_1:1;
then Y is Subset of S;
then ex_inf_of Y, S & x = "/\"(Y,S) by YELLOW_0:39,55;
hence thesis by A4;
end;
then A12: f.:X c= f.:Z by RELAT_1:156;
A13: f.:Z is_>=_than f.inf X by A10,YELLOW_0:31;
A14: f.:X is_>=_than f.inf X
proof let x be Element of T; assume x in f.:X;
hence thesis by A12,A13,LATTICE3:def 8;
end;
A15: now let b be Element of T; assume
A16: 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 set such that
A17: x in dom f & x in Z & a = f.x by FUNCT_1:def 12;
consider Y being non empty finite Subset of X such that
A18: ex_inf_of Y, S & x = "/\"(Y,S) by A4,A17;
Y is Subset of S by XBOOLE_1:1;
then reconsider Y as Subset of S;
f.:Y c= f.:X & f preserves_inf_of Y by A1,Th2,RELAT_1:156;
then b is_<=_than f.:Y & a = "/\"(f.:Y,T) & ex_inf_of f.:Y, T
by A16,A17,A18,WAYBEL_0:def 30,YELLOW_0:9;
hence thesis by YELLOW_0:def 10;
end;
hence f.inf X >= b by A10,YELLOW_0:31;
end;
hence ex_inf_of f.:X,T by A14,YELLOW_0:16;
hence inf (f.:X) = f.inf X by A14,A15,YELLOW_0:def 10;
end;
theorem Th5:
for S,T being Semilattice, f being map of S,T st f is infs-preserving
holds f is SemilatticeHomomorphism of S,T
proof let S,T be Semilattice, f be map of S,T such that
A1: f is infs-preserving;
{} c= the carrier of S by XBOOLE_1:2;
then reconsider e = {} as Subset of S;
hereby assume S is upper-bounded;
then ex_inf_of e, S & f preserves_inf_of e
by A1,WAYBEL_0:def 32,YELLOW_0:43;
then ex_inf_of f.:e, T & f.:e = {} by RELAT_1:149,WAYBEL_0:def 30;
hence T is upper-bounded by WAYBEL20:5;
end;
let X be finite Subset of S; thus thesis by A1,WAYBEL_0:def 32;
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 map of S1,T1, f2 being map 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 & the RelStr of T1 = the RelStr of T2;
let f1 be map of S1,T1, f2 be map of S2,T2 such that
A2: f1 = f2;
thus f1 is infs-preserving implies f2 is infs-preserving
proof assume
A3: for X being Subset of S1 holds f1 preserves_inf_of X;
let X be Subset of S2;
reconsider Y = X as Subset of S1 by A1;
f1 preserves_inf_of Y by A3;
hence thesis by A1,A2,WAYBEL_0:65;
end;
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 Y is non empty directed by A1,WAYBEL_0:3;
then f1 preserves_sup_of Y by A4;
hence thesis by A1,A2,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 map of S1,T1, f2 being map 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 & the RelStr of T1 = the RelStr of T2;
let f1 be map of S1,T1, f2 be map of S2,T2 such that
A2: f1 = f2;
thus f1 is sups-preserving implies f2 is sups-preserving
proof assume
A3: for X being Subset of S1 holds f1 preserves_sup_of X;
let X be Subset of S2;
reconsider Y = X as Subset of S1 by A1;
f1 preserves_sup_of Y by A3;
hence thesis by A1,A2,WAYBEL_0:65;
end;
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 Y is non empty filtered by A1,WAYBEL_0:4;
then f1 preserves_inf_of Y by A4;
hence thesis by A1,A2,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 f = id the carrier of S by YELLOW_9:def 1;
then A1: f.:X = X & ex_inf_of X, T & f.inf X = inf X
by BORSUK_1:3,FUNCT_1:35,YELLOW_0:17;
then "/\"(X,T) in the carrier of S by YELLOW_0:def 18;
hence thesis by A1,YELLOW_0:64;
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 f = id the carrier of S by YELLOW_9:def 1;
then A1: f.:X = X & ex_sup_of X, T & f.sup X = sup X
by BORSUK_1:3,FUNCT_1:35,YELLOW_0:17;
then "\/"(X,T) in the carrier of S by YELLOW_0:def 19;
hence thesis by A1,YELLOW_0:65;
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
A1: X is non empty directed & ex_sup_of X, S;
then reconsider X' = X as non empty directed Subset of T by YELLOW_2:7;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then f = id the carrier of S by YELLOW_9:def 1;
then A2: f.:X = X' & f.sup X = sup X by BORSUK_1:3,FUNCT_1:35;
hence ex_sup_of f.:X, T by WAYBEL_0:75;
hence thesis by A1,A2,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
A1: X is non empty filtered & 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 f = id the carrier of S by YELLOW_9:def 1;
then f.:X = X & ex_inf_of X, T & f.inf X = inf X
by BORSUK_1:3,FUNCT_1:35,YELLOW_0:17;
hence thesis by A1,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 & the RelStr of S = the RelStr of R;
thus
A2: R is SubRelStr of T2
proof thus the carrier of R c= the carrier of T2 &
the InternalRel of R c= the InternalRel of T2 by A1,YELLOW_0:def 13;
end;
assume the InternalRel of S = (the InternalRel of T)|_2 the carrier of S;
hence thesis by A1,A2,YELLOW_0: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:15;
A1: R is infs-inheriting
proof let X be Subset of R;
thus thesis;
end;
R is sups-inheriting
proof let X be Subset of R;
thus thesis;
end;
hence thesis by A1;
end;
definition
let T be complete LATTICE;
cluster complete 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
A5: y in X & x c= X & P[x];
thus P[x \/ {y}]
proof assume x \/ {y} <> {};
reconsider y' = y as Element of S by A5;
reconsider z = y' as Element of T by YELLOW_0:59;
x c= the carrier of S & the carrier of S c= the carrier of T
by A5,XBOOLE_1:1,YELLOW_0:def 13;
then x c= the carrier of T by XBOOLE_1:1;
then reconsider x' = x as finite Subset of T
by A5,FINSET_1:13;
A6: ex_inf_of {z}, T & inf {z} = y' by YELLOW_0:38,39;
now assume
A7: x' <> {};
then ex_inf_of x', T by YELLOW_0:55;
then A8: inf x' in the carrier of S & inf (x' \/ {z}) = (inf x')"/\"z &
ex_inf_of {inf x', z}, T by A5,A6,A7,YELLOW_0:21,YELLOW_2:4;
then inf {inf x', z} in the carrier of S by A1,YELLOW_0:def 16;
hence inf (x' \/ {z}) in the carrier of S by A8,YELLOW_0:40;
end;
hence "/\"(x \/ {y}, T) in the carrier of S by A6;
end;
end;
P[X] from Finite(A2,A3,A4);
hence "/\"(X, T) in the carrier of S;
end;
assume
A9: 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 x in the carrier of S & y in the carrier of S;
then {x,y} c= the carrier of S by ZFMISC_1:38;
then {x,y} is finite non empty Subset of S;
hence thesis by A9;
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
A5: y in X & x c= X & P[x];
then reconsider y' = y as Element of S;
reconsider z = y' as Element of T by YELLOW_0:59;
thus P[x \/ {y}]
proof assume x \/ {y} <> {};
x c= the carrier of S & the carrier of S c= the carrier of T
by A5,XBOOLE_1:1,YELLOW_0:def 13;
then x c= the carrier of T by XBOOLE_1:1;
then reconsider x' = x as finite Subset of T
by A5,FINSET_1:13;
A6: ex_sup_of {z}, T & sup {z} = y' by YELLOW_0:38,39;
now assume
A7: x' <> {};
then ex_sup_of x', T by YELLOW_0:54;
then
A8: sup x' in the carrier of S & sup (x' \/ {z}) = (sup x')"\/"z &
ex_sup_of {sup x', z}, T by A5,A6,A7,YELLOW_0:20,YELLOW_2:3;
then sup {sup x', z} in the carrier of S by A1,YELLOW_0:def 17;
hence sup (x' \/ {z}) in the carrier of S by A8,YELLOW_0:41;
end;
hence "\/"(x \/ {y}, T) in the carrier of S by A6;
end;
end;
P[X] from Finite(A2,A3,A4);
hence "\/"(X, T) in the carrier of S;
end;
assume
A9: 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 x in the carrier of S & y in the carrier of S;
then {x,y} c= the carrier of S by ZFMISC_1:38;
then {x,y} is finite non empty Subset of S;
hence thesis by A9;
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 & 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 A c= the carrier of T by XBOOLE_1:1;
then reconsider C = A as Subset of T;
set F = fininfs C;
assume
A2: ex_inf_of A, T;
then A3: inf F = inf C by WAYBEL_0:60;
A4: F = {"/\"(Y,T) where Y is finite Subset of C: ex_inf_of Y, T}
by WAYBEL_0:def 28;
F c= the carrier of S
proof let x be set; assume x in F;
then consider Y being finite Subset of C such that
A5: x = "/\"(Y, T) & ex_inf_of Y, T by A4;
Y c= the carrier of T by XBOOLE_1:1;
then reconsider Y as finite Subset of T;
Y c= the carrier of S by XBOOLE_1:1;
then reconsider Z = Y as finite Subset of S;
assume
A6: not x in the carrier of S;
then Z <> {} by A1,A5,YELLOW_0:def 12;
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:24;
A7: now let Y be finite Subset of C;
Y c= the carrier of T by XBOOLE_1:1;
then Y is Subset of T;
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 by A4
;
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;
Y c= the carrier of T by XBOOLE_1:1;
then reconsider Z = Y as finite Subset of T;
assume Y <> {}; then ex_inf_of Z, T by YELLOW_0:55;
hence "/\"(Y,T) in F by A4;
end;
then ex_inf_of G, T by A2,A7,A8,WAYBEL_0:58;
hence "/\"(A, T) in the carrier of S by A1,A3,WAYBEL_0:def 3;
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 & 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 A c= the carrier of T by XBOOLE_1:1;
then reconsider C = A as Subset of T;
set F = finsups C;
assume
A2: ex_sup_of A, T;
then A3: sup F = sup C by WAYBEL_0:55;
A4: F = {"\/"(Y,T) where Y is finite Subset of C: ex_sup_of Y, T}
by WAYBEL_0:def 27;
F c= the carrier of S
proof let x be set; assume x in F;
then consider Y being finite Subset of C such that
A5: x = "\/"(Y, T) & ex_sup_of Y, T by A4;
Y c= the carrier of T by XBOOLE_1:1;
then reconsider Y as finite Subset of T;
Y c= the carrier of S by XBOOLE_1:1;
then reconsider Z = Y as finite Subset of S;
assume
A6: not x in the carrier of S;
then Z <> {} by A1,A5,YELLOW_0:def 11;
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:24;
A7: now let Y be finite Subset of C;
Y c= the carrier of T by XBOOLE_1:1;
then Y is Subset of T;
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 by A4
;
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;
Y c= the carrier of T by XBOOLE_1:1;
then reconsider Z = Y as finite Subset of T;
assume Y <> {}; then ex_sup_of Z, T by YELLOW_0:54;
hence "\/"(Y,T) in F by A4;
end;
then ex_sup_of G, T by A2,A7,A8,WAYBEL_0:53;
hence "\/"(A, T) in the carrier of S by A1,A3,WAYBEL_0:def 4;
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;
Y c= the carrier of S by XBOOLE_1:17;
then reconsider Y as Subset of S;
A2: ex_inf_of Y, T by YELLOW_0:17;
then "/\"(Y,T) in the carrier of S by A1,YELLOW_0:def 18;
then ex_inf_of Y, S by A2,YELLOW_0:64;
hence ex_inf_of X, S by YELLOW_0:50;
end;
hence thesis by YELLOW_2:27;
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;
Y c= the carrier of S by XBOOLE_1:17;
then reconsider Y as Subset of S;
A2: ex_sup_of Y, T by YELLOW_0:17;
then "\/"(Y,T) in the carrier of S by A1,YELLOW_0:def 19;
then ex_sup_of Y, S by A2,YELLOW_0:65;
hence ex_sup_of X, S by YELLOW_0:50;
end;
hence thesis by YELLOW_2: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 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 ex_inf_of Y,T1 by A1,YELLOW_0:14;
then "/\"(Y,T1) in the carrier of S1 by A3;
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 ex_sup_of Y,T1 by A1,YELLOW_0:14;
then "\/"(Y,T1) in the carrier of S1 by A3;
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:58;
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 ex_sup_of Y,T1 by A1,YELLOW_0:14;
then "\/"(Y,T1) in the carrier of S1 by A4,A5;
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:58;
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 ex_inf_of Y,T1 by A1,YELLOW_0:14;
then "/\"(Y,T1) in the carrier of S1 by A4,A5;
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 map 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;
let f be map of S,T such that
A1: f is continuous;
let p be set; assume
A2: p in f.:Lim N; then reconsider p as Point of T;
consider x being set such that
A3: x in the carrier of S & x in Lim N & p = f.x by A2,FUNCT_2:115;
reconsider x as Element of S by A3;
now let V be a_neighborhood of p;
p in Int V & Int V is open by CONNSP_2:def 1,TOPS_1:51;
then x in f"Int V & f"Int V is open by A1,A3,FUNCT_2:46,TOPS_2:55;
then f"Int V is a_neighborhood of x by CONNSP_2:5;
then N is_eventually_in f"Int V by A3,YELLOW_6:def 18;
then consider i being Element of N such that
A4: for j being Element of N st j >= i holds N.j in
f"Int V by WAYBEL_0:def 11;
A5: the mapping of f*N = f*the mapping of N &
the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
then reconsider i' = i as Element of f*N;
thus f*N is_eventually_in V
proof take i'; let j' be Element of f*N;
reconsider j = j' as Element of N by A5;
A6: f.(N.j) = f.((the mapping of N).j) by WAYBEL_0:def 8
.= (f*the mapping of N).j by FUNCT_2:21
.= (f*N).j' by A5,WAYBEL_0:def 8;
assume j' >= i'; then j >= i by A5,YELLOW_0:1;
then N.j in f"Int V by A4;
then f.(N.j) in Int V & Int V c= V by FUNCT_2:46,TOPS_1:44;
hence thesis by A6;
end;
end;
hence thesis by YELLOW_6:def 18;
end;
definition
let T be non empty RelStr;
let N be non empty NetStr over T;
redefine attr N is antitone means:
Def2:
for i,j being Element of N st i <= j holds N.i >= N.j;
compatibility
proof
A1: netmap(N,T) = the mapping of N by WAYBEL_0:def 7;
hereby assume N is antitone;
then A2: netmap(N,T) is antitone by WAYBEL_0:def 10;
let i,j be Element of N; assume i <= j;
then netmap(N,T).i >= netmap(N,T).j by A2,WAYBEL_0:def 5;
then N.i >= netmap(N,T).j by A1,WAYBEL_0:def 8;
hence N.i >= N.j by A1,WAYBEL_0:def 8;
end;
assume
A3: for i,j being Element of N st i <= j holds N.i >= N.j;
let i,j be Element of N;
N.i = netmap(N,T).i & N.j = netmap(N,T).j
by A1,WAYBEL_0:def 8;
hence thesis by A3;
end;
end;
definition
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 & k = x by A1,TARSKI:def 1;
hence thesis by YELLOW_0:def 1;
end;
thus N is directed
proof let i,j be Element of N; i = x & j = x by A1,TARSKI:def 1;
then i <= i & j <= i;
hence thesis;
end;
thus N is monotone
proof let i,j be Element of N; i = x & j = x by A1,TARSKI:def 1;
hence thesis by YELLOW_0:def 1;
end;
let i,j be Element of N; i = x & j = x by A1,TARSKI:def 1;
hence thesis by YELLOW_0:def 1;
end;
end;
definition
let T be non empty reflexive RelStr;
cluster monotone antitone reflexive strict net of T;
existence
proof consider x being Element of T;
take {x} opp+id; thus thesis;
end;
end;
definition
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:59;
assume i <= j; then x <= y by A1,YELLOW_0:60;
then ~x >= ~y & ~x = x by LATTICE3:def 7,YELLOW_7:1;
then (F opp+id).i >= ~y & ~y = y by LATTICE3:def 7,YELLOW_9:7;
hence (F opp+id).i >= (F opp+id).j by YELLOW_9:7;
end;
end;
definition
let S,T be non empty reflexive RelStr;
let f be monotone map 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 &
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 A1,YELLOW_0:1;
then N.x >= N.y by Def2;
then f.(N.x) >= f.(N.y) & N.x = (the mapping of N).x &
(f*N).i = (the mapping of f*N).i by WAYBEL_0:def 8,WAYBEL_1:def 2;
then (f*N).i >= f.(N.y) & N.y = (the mapping of N).y &
(f*N).j = (the mapping of f*N).j by A1,FUNCT_2:21,WAYBEL_0:def 8;
hence thesis by A1,FUNCT_2:21;
end;
end;
theorem Th25:
for S being complete LATTICE, N be net of S holds
{"/\"({N.i where i is Element of N:i >= j},S)
where j is Element of N: not contradiction}
is directed non empty Subset of S
proof let S be complete LATTICE, N be net of S;
set X = {"/\"({N.i where i is Element of N:i >= j},S)
where j is Element of N: not contradiction};
X c= the carrier of S
proof let x be set; 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
{"/\"({N.i where i is Element of N: i >= j}, S)
where j is Element of N: not contradiction}
is directed non empty Subset of S
proof let S be non empty Poset, N be monotone reflexive net of S;
set X = {"/\"({N.i where i is Element of N: i >= j}, S)
where j is Element of N: not contradiction};
consider jj being 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 set; 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 & [#]N = the carrier of N
by PRE_TOPC:12,WAYBEL_0:def 6;
then consider j being Element of N such that
A4: j in [#]N & j >= j1 & j >= j2 by WAYBEL_0:def 1;
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};
A5: for j being Element of N holds ex_inf_of up(j), S
proof let j be Element of N;
reconsider j' = j as Element of N;
now take x = N.j;
j' <= j';
then A6: 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 A6,LATTICE3:def 8;
end;
hence thesis by YELLOW_0:16;
end;
then A7: ex_inf_of up(j1), S;
A8: ex_inf_of up(j2), S by A5;
A9: ex_inf_of up(j), S by A5;
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 set; assume a in A;
then consider k being Element of N such that
A10: a = N.k & k >= j;
reconsider k as Element of N;
k >= j1 by A4,A10,ORDERS_1:26;
hence thesis by A10;
end;
hence z >= x by A2,A7,A9,YELLOW_0:35;
A c= {N.k where k is Element of N:k >= j2}
proof let a be set; assume a in A;
then consider k being Element of N such that
A11: a = N.k & k >= j;
reconsider k as Element of N;
k >= j2 by A4,A11,ORDERS_1:26;
hence thesis by A11;
end;
hence z >= y by A3,A8,A9,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;
consider i being Element of N;
take i; let j be Element of N;
N.j = (the mapping of N).j by WAYBEL_0:def 8;
then N.j in rng the mapping of N by FUNCT_2:6;
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 set; assume x in X;
then consider i being Element of N such that
A4: x = N.i & i >= v;
reconsider i as Element of N;
x = i by A4,YELLOW_9:7;
hence thesis by A2;
end;
then A5: X c= the carrier of R by XBOOLE_1:1;
vv <= vv;
then N.v in X;
then reconsider X as non empty Subset of R by A5;
A6: ex_inf_of F, R & ex_inf_of X, R by WAYBEL_0:76;
then A7: inf X >= inf F by A3,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 & a >= b & j >= b by A2,WAYBEL_0:def 2;
reconsider k = b as Element of N by A2,A8;
N is full SubRelStr of R opp & j~ = v & b~ = k & j~ <= b~
by A8,LATTICE3:9,def 6,YELLOW_9:7;
then N.k = b & k >= vv by YELLOW_0:61,YELLOW_9:7;
then b in X;
then {b} c= X & ex_inf_of {b}, R & inf {b} = b
by YELLOW_0:38,39,ZFMISC_1:37;
then b >= inf X by A6,YELLOW_0:35;
hence thesis by A8,YELLOW_0:def 2;
end;
then inf F >= "/\"(X, R) by A6,YELLOW_0:31;
hence thesis by A7,ORDERS_1:25;
end;
A9: {F(j) where j is Element of N: P[j]}
= {G(k) where k is Element of N: P[k]}
from FraenkelF'R(A1);
A10: ex j being Element of N st P[j];
{inf F where j is Element of N: P[j]}
= {inf F} from SingleFraenkel(A10);
hence lim_inf N = "\/"({inf F}, R) by A9,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 map 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 map 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 &
the mapping of N = f*the mapping of M by WAYBEL_9:def 8;
A2: the carrier of M = X & the mapping of M = id X by WAYBEL19:27,YELLOW_9:7;
defpred P[set] means not contradiction;
deffunc G(set) = inf (f.:X);
A3: 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;
A4: [#]N is directed & [#]N = the carrier of N
by PRE_TOPC:12,WAYBEL_0:def 6;
then consider i' being Element of N such that
A5: i' in [#]N & i' >= j & i' >= j by WAYBEL_0:def 1;
A6: up(j) c= f.:X
proof let a be set; assume a in up(j);
then consider i being Element of N such that
A7: a = N.i & i >= j;
reconsider i as Element of N;
reconsider i' = i as Element of M by A1;
A8: N.i = (the mapping of N).i by WAYBEL_0:def 8
.= f.((id X).i) by A1,A2,FUNCT_2:21
.= f.i' by A2,FUNCT_1:35;
i' in X & the carrier of T <> {} by A2;
hence thesis by A7,A8,FUNCT_2:43;
end;
then up(j) c= the carrier of T & N.i' in up(j) by A5,XBOOLE_1:1;
then up(j) is non empty Subset of T;
then A9: ex_inf_of up(j), T & ex_inf_of f.:X, T by WAYBEL_0:76;
then A10: infy(j) >= inf (f.:X) by A6,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 set such that
A11: y in the carrier of S & y in X & x = f.y by FUNCT_2:115;
reconsider y as Element of N by A1,A2,A11;
consider i being Element of N such that
A12: i in [#]N & i >= y & i >= j by A4,WAYBEL_0:def 1;
i in X by A1,A2;
then reconsider xi = i, xy = y as Element of S by A11;
M is full SubRelStr of S opp by YELLOW_9:7;
then N is full SubRelStr of S opp & xi = xi~ & xy = xy~
by A1,Th12,LATTICE3:def 6;
then xi~ >= xy~ by A12,YELLOW_0:60;
then xi <= xy by LATTICE3:9;
then A13: f.xi <= x by A11,WAYBEL_1:def 2;
N.i = (the mapping of N).i by WAYBEL_0:def 8
.= f.((id X).i) by A1,A2,FUNCT_2:21
.= f.xi by A1,A2,FUNCT_1:35;
then f.xi in up(j) by A12;
then f.xi >= infy(j) by A9,YELLOW_4:2;
hence thesis by A13,ORDERS_1:26;
end;
then infy(j) <= inf (f.:X) by A9,YELLOW_0:31;
hence thesis by A10,ORDERS_1:25;
end;
A14: 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 FraenkelF'R(A3)
.= {inf (f.:X) where j is Element of N: P[j]}
.= {inf (f.:X)} from SingleFraenkel(A14);
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 map 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 map 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 &
the mapping of N = f*the mapping of X opp+id by WAYBEL_9:def 8;
A3: the carrier of M = Y &
M is full SubRelStr of T opp &
the mapping of M = id Y by WAYBEL19:27,YELLOW_9:7;
A4: the carrier of X opp+id = X & X opp+id is full SubRelStr of S opp &
the mapping of X opp+id = id X by WAYBEL19:27,YELLOW_9:7;
then A5: the mapping of N = f|X & the carrier of T <> {} by A2,RELAT_1:94;
then A6: rng the mapping of N = f.:X & dom the mapping of N = X
by A2,A4,FUNCT_2:def 1,RELAT_1:148;
then the mapping of N is Function of the carrier of N, Y
by A1,A2,A4,FUNCT_2:def 1,RELSET_1:11;
then reconsider g = f|X as map of N,M by A3,A5;
take g;
thus the mapping of N = (the mapping of M)*g by A1,A3,A5,A6,RELAT_1:79;
let m be Element of M;
consider n being set such that
A7: n in the carrier of S & n in X & m = f.n by A1,A3,FUNCT_2:115;
reconsider n as Element of N by A2,A4,A7;
take n; let p be Element of N;
p in X by A2,A4;
then reconsider n' = n, p' = p as Element of S by A7;
f.p' in the carrier of M by A1,A2,A3,A4,FUNCT_2:43;
then reconsider fp = f.p' as Element of M;
X opp+id is SubRelStr of S opp by YELLOW_9:7;
then A8: N is SubRelStr of S opp & n'~ = n' & p'~ = p' by A2,Th12,LATTICE3:def
6;
A9: M is full SubRelStr of T opp by YELLOW_9:7;
assume n <= p;
then n'~ <= p'~ by A8,YELLOW_0:60;
then n' >= p' by LATTICE3:9;
then f.n' >= f.p' by WAYBEL_1:def 2;
then (f.n')~ <= (f.p')~ & (f.n')~ = m & (f.p')~ = fp &
the carrier of M <> {} by A7,LATTICE3:9,def 6;
then fp >= m by A9,YELLOW_0:61;
hence m <= g.p by A2,A4,FUNCT_1:72;
end;
theorem
for S,T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone map 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 map 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:41;
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;
dom id D = D & rng id D = D by RELAT_1:71;
then reconsider g = id D as Function of D, the carrier of S
by FUNCT_2:def 1,RELSET_1:11;
(id the carrier of S)|D = id D by FUNCT_3:1;
then A1: 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 WELLORD1:15;
hence thesis by A1,YELLOW_0:def 13,def 14;
end;
theorem Th33:
for S,T being up-complete (non empty Poset)
for f being monotone map 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 map 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 = {infy(j) where j is Element of N:
not contradiction};
A1: the RelStr of N = the RelStr of M &
the mapping of N = f*the mapping of M by WAYBEL_9:def 8;
A2: the carrier of M = X & the mapping of M = id X by Th32;
A3: now let i be Element of N;
thus N.i = (the mapping of N).i by WAYBEL_0:def 8
.= f.((id X).i) by A1,A2,FUNCT_2:21
.= f.i by A1,A2,FUNCT_1:35;
end;
A4: for i being Element of N holds infy(i) = f.i
proof let i be Element of N;
i in X by A1,A2;
then reconsider x = i as Element of S;
A5: i <= i;
N.i = f.x by A3;
then f.x in up(i) by A5;
then A6: for z being Element of T st z is_<=_than up(i) holds z <= f.x
by LATTICE3:def 8;
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
A7: z = N.j & j >= i;
reconsider j as Element of N;
j in X by A1,A2;
then reconsider y = j as Element of S;
M is full SubRelStr of S & the RelStr of S = the RelStr of S
by Th32;
then N is full SubRelStr of S by A1,Th12;
then y >= x by A7,YELLOW_0:60;
then f.y >= f.x by WAYBEL_1:def 2;
hence thesis by A3,A7;
end;
hence "/\"(up(i), T) = f.i by A6,YELLOW_0:31;
end;
NT = f.:X
proof
thus NT c= f.:X
proof let x be set; assume x in NT;
then consider j being Element of N such that
A8: x = infy(j);
reconsider j as Element of N;
x = f.j & j in X & the carrier of T <> {} by A1,A2,A4,A8;
hence thesis by FUNCT_2:43;
end;
let y be set; assume y in f.:X;
then consider x being set such that
A9: x in the carrier of S & x in X & y = f.x by FUNCT_2:115;
reconsider x as Element of S by A9;
reconsider i = x as Element of N by A1,A2,A9;
f.x = infy(i) by A4;
hence thesis by A9;
end;
hence lim_inf N = sup (f.:X) 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;
dom id D = D & rng id D = D by RELAT_1:71;
then reconsider g = id D as Function of D, the carrier of S
by FUNCT_2:def 1,RELSET_1:11;
(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 & the carrier of N = D by Th32;
consider K being prebasis of T;
now let A be Subset of T; assume
A2: sup D in A;
A3: K c= the topology of T by CANTOR_1:def 5;
assume A in K; then A is open by A3,PRE_TOPC:def 5;
then A has_the_property_(S) by WAYBEL19:36;
then consider y being Element of T such that
A4: y in D and
A5: for x being Element of T st x in D & x >= y holds x in A
by A2,WAYBEL11:def 3;
reconsider i = y as Element of N by A1,A4;
thus N is_eventually_in A
proof take i; let j be Element of N;
N.j = (the mapping of N).j & N.i = (the mapping of N).i
by WAYBEL_0:def 8;
then A6: j = N.j & y = N.i by A1,FUNCT_1:34;
assume j >= i;
then N.j >= N.i by Th34;
hence thesis by A1,A5,A6;
end;
end;
hence sup D in Lim N 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 -> map 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 12;
end;
theorem Th36:
for T being non empty 1-sorted
for N being net of T, M being non empty 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 non empty 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 M.i = ((the mapping of N)*e).i by WAYBEL_0:def 8
.= (the mapping of N).(e.i) by FUNCT_2:21
.= N.(e.i) by WAYBEL_0:def 8;
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) = {"/\"
({$1.i where i is Element of $1:
i >= j}, T) where j is Element of $1: not contradiction};
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);
consider e being Embedding of M,N;
reconsider j as Element of N;
consider j' being Element of M such that
A3: for p being Element of M st j' <= 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 >= j'};
A4: ex_inf_of X, T & ex_inf_of Y, T by YELLOW_0:17;
Y c= X
proof let y be set; assume y in Y;
then consider i being Element of M such that
A5: y = M.i & i >= j';
reconsider i as Element of M;
e.i >= j by A3,A5;
then N.(e.i) in X;
hence thesis by A5,Th36;
end;
then A6: t <= "/\"(Y, T) by A2,A4,YELLOW_0:35;
"/\"(Y, T) in infy(M);
then "/\"(Y, T) <= "\/"(infy(M), T) by YELLOW_2:24;
hence thesis by A6,YELLOW_0:def 2;
end;
lim_inf M = "\/"(infy(M), T) & lim_inf N = "\/"(infy(N), T)
by WAYBEL11:def 6;
hence thesis by A1,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 j' being Element of M st j' >= j & N.i >= M.j'
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 j' being Element of M st j' >= j & N.i >= M.j';
deffunc infy(net of T) = {"/\"
({$1.i where i is Element of $1:
i >= j}, T) where j is Element of $1: not contradiction};
"\/"(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 j' = e.j;
set X = {N.i where i is Element of N: i >= j'};
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 & i >= j';
reconsider i as Element of N;
consider k being Element of M such that
A4: k >= j & N.i >= M.k by A1,A3;
M.k in Y by A4;
then M.k >= t by A2,YELLOW_2:24;
hence thesis by A3,A4,YELLOW_0:def 2;
end;
then A5: t <= "/\"(X, T) by YELLOW_0:33;
"/\"(X, T) in infy(N);
then "/\"(X, T) <= "\/"(infy(N), T) by YELLOW_2:24;
hence t <= "\/"(infy(N), T) by A5,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 lim_inf N >= lim_inf M & lim_inf M >= lim_inf N by Th37,WAYBEL11:def 6
;
hence thesis by 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 &
M is full SubRelStr of N by YELLOW_6:def 8,def 9;
then A3: 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 A2,YELLOW_0:59;
consider k being Element of N such that
A4: k >= i & k >= j by YELLOW_6:def 5;
consider l being Element of N such that
A5: l >= k & l in the carrier of M by A1;
reconsider z = l as Element of M by A5;
take z;
l >= i & l >= j by A4,A5,YELLOW_0:def 2;
hence thesis by YELLOW_6:21;
end;
then reconsider K = M as net of T by A2;
A6: now set f = incl(K,N);
A7: f = id the carrier of K by A3,YELLOW_9:def 1;
hence the mapping of K = (the mapping of N)*f by A2,RELAT_1:94;
let m be Element of N;
consider j being Element of N such that
A8: j >= m & j in the carrier of K by A1;
reconsider n = j as Element of K by A8;
take n; let p be Element of K;
reconsider q = p as Element of N by A2,YELLOW_0:59;
assume n <= p; then j <= q & f.p = q by A7,FUNCT_1:35,YELLOW_6:20;
hence m <= f.p by A8,YELLOW_0:def 2;
end;
hence M is subnet of N by YELLOW_6:def 12;
hence thesis by A6,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 9;
the carrier of N|i c= the carrier of N by WAYBEL_9:13;
then A2: incl(N|i,N) = id the carrier of N|i by 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:94;
let m be Element of N;
consider n' being Element of N such that
A3: n' >= i & n' >= m by YELLOW_6:def 5;
n' in the carrier of M by A3,WAYBEL_9:def 7;
then reconsider n = n' as Element of M;
take n;
let p be Element of M; reconsider p' = p as Element of N by A1,YELLOW_0:59;
assume n <= p; then n' <= p' by A1,YELLOW_0:60;
then m <= p' by A3,YELLOW_0:def 2;
hence m <= f.p by A2,FUNCT_1:35;
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 9;
the carrier of M c= the carrier of N by WAYBEL_9:13;
then A2: incl(M,N) = id the carrier of M by YELLOW_9:def 1;
now let k be Element of N, j be Element of M;
consider j' being Element of N such that
A3: j' = j & j' >= i by WAYBEL_9:def 7;
assume e.j <= k;
then A4: k >= j' by A2,A3,FUNCT_1:35;
then k >= i by A3,YELLOW_0:def 2;
then k in the carrier of M by WAYBEL_9:def 7;
then reconsider k' = k as Element of M;
take k'; thus k' >= j by A1,A3,A4,YELLOW_0:61;
M.k' = N.(e.k') & M.k' <= M.k' by Th36;
hence N.k >= M.k' by A2,FUNCT_1:35;
end;
hence lim_inf (N|i) = lim_inf N 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 i' being Element of N such that
A1: for j being Element of N st j >= i' holds N.j in X;
[#]N is directed & [#]
N = the carrier of N by PRE_TOPC:12,WAYBEL_0:def 6;
then consider i being Element of N such that
A2: i in [#]N & i' <= i & i' <= i by WAYBEL_0:def 1;
take i; thus N.i in X by A1,A2;
let x be set; assume x in rng the mapping of N|i;
then consider j being set such that
A3: j in dom the mapping of N|i & x = (the mapping of N|i).j by FUNCT_1:def 5;
A4: dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1;
then 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
A5: j = k & i <= k by A3,A4;
A6: i' <= k by A2,A5,ORDERS_1:26;
x = (N|i).j by A3,WAYBEL_0:def 8 .= N.k by A5,WAYBEL_9:16;
hence thesis by A1,A6;
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 set such that
A1: i1 in dom the mapping of N & x = (the mapping of N).i1 by FUNCT_1:def 5;
assume y in F;
then consider i2 being set such that
A2: i2 in dom the mapping of N & y = (the mapping of N).i2 by FUNCT_1:def 5;
A3: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
then reconsider i1, i2 as Element of N by A1,A2;
consider j1 being Element of N such that
A4: 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
A5: 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
A6: j2 <= j & j1 <= j by YELLOW_6:def 5;
take z = N.j; z = (the mapping of N).j by WAYBEL_0:def 8;
hence z in F by A3,FUNCT_1:def 5;
x = N.i1 & y = N.i2 by A1,A2,WAYBEL_0:def 8;
hence thesis by A4,A5,A6;
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);
consider S being 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;
A5: now let i be Element of N;
N.i = (the mapping of N).i by WAYBEL_0:def 8;
hence N.i in F by A4,FUNCT_1:def 5;
end;
thus Lim N c= {inf N}
proof let p be set; assume
A6: 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 set such that
A7: i in dom the mapping of N & u = (the mapping of N).i by FUNCT_1:def 5
;
reconsider i as Element of N by A4,A7;
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:52;
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;
then N.j <= u by A7,WAYBEL_0:def 8;
hence thesis by WAYBEL_0:17;
end;
then Lim N c= downarrow u by A9,WAYBEL19:26;
hence thesis by A6,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:52;
then A12: Cl F c= uparrow inf N by A11,PRE_TOPC:49;
p in Cl F by A6,WAYBEL_9:24;
then p >= inf N by A12,WAYBEL_0:18;
then p = inf N by A10,ORDERS_1:25;
hence thesis by TARSKI:def 1;
end;
reconsider K = (sigma T) \/
{(uparrow x)` where x is Element of T: not contradiction} as prebasis of T
by WAYBEL19:30;
now let A be Subset of T; assume
A13: inf F in A & A in K;
per cases by A13,XBOOLE_0:def 2;
suppose
A14: A in sigma T;
then reconsider a = A as Subset of S by A1;
a is open by A1,A14,PRE_TOPC:def 5;
then a is upper by WAYBEL11:def 4;
then A15: A is upper by A2,WAYBEL_0:25;
consider i being Element of N;
thus N is_eventually_in A
proof take i; let j be Element of N;
N.j in F by A5;
then N.j >= inf F by YELLOW_2:24;
hence thesis by A13,A15,WAYBEL_0:def 20;
end;
suppose A in {(uparrow x)` where x is Element of T: not contradiction};
then consider x being Element of T such that
A16: A = (uparrow x)`;
not inf F >= x by A13,A16,YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A17: y in F & not y >= x by LATTICE3:def 8;
consider i being set such that
A18: i in the carrier of N & y = (the mapping of N).i by A4,A17,FUNCT_1:def
5;
thus N is_eventually_in A
proof
reconsider i as Element of N by A18;
consider ii being Element of N such that
A19: 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 & N.i = y by A18,A19,WAYBEL_0:def 8;
then not N.j >= x by A17,ORDERS_1:26;
hence N.j in A by A16,YELLOW_9:1;
end;
end;
then inf F in Lim N by WAYBEL19:25;
hence thesis by A3,ZFMISC_1:37;
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 map 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);
consider Ss being Scott TopAugmentation of S,
Ts being Scott TopAugmentation of T,
Sl being lower correct TopAugmentation of S,
Tl being lower correct TopAugmentation of T;
S is TopAugmentation of S & T is TopAugmentation of T by YELLOW_9:44;
then A1: S is Refinement of Ss,Sl & T is Refinement of Ts,Tl by WAYBEL19:29;
A2: T is TopAugmentation of Ts & S is TopAugmentation of Ss by YELLOW_9:45;
A3: the RelStr of Ss = the RelStr of S & the RelStr of Sl = the RelStr of S &
the RelStr of Ts = the RelStr of T & the RelStr of Tl = the RelStr of T
by YELLOW_9:def 4;
let f be meet-preserving map of S,T;
reconsider g = f as map of Sl,Tl by A3;
reconsider h = f as map of Ss,Ts by A3;
hereby assume
A4: 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 A3;
assume
A5: P is open;
then C is open by A2,WAYBEL19:37;
then A6: f"C is open by A4,TOPS_2:55;
A is upper & h is monotone by A3,A5,WAYBEL11:def 4,WAYBEL_9:1;
then h"A is upper by WAYBEL17:2;
then f"C is upper by A3,WAYBEL_0:25;
hence h"P is open by A2,A6,WAYBEL19:41;
end;
then h is continuous by TOPS_2:55;
then h is directed-sups-preserving by WAYBEL17:22;
hence f is directed-sups-preserving by A3,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 f.:{inf F} c= Lim (f*(F opp+id)) &
f is Function of the carrier of S, the carrier of T by A4,Th24;
then {f.inf F} c= Lim (f*(F opp+id)) by SETWISEO:13;
then A7: f.inf F in Lim (f*(F opp+id)) by ZFMISC_1:37;
reconsider G = f.:F as filtered non empty Subset of T by WAYBEL20:25;
A8: 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:94
.= G by RELAT_1:148;
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 A8,YELLOW_2:def 6;
hence thesis by A7,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 h is directed-sups-preserving by A3,Th6;
then A9: h is continuous by WAYBEL17:22;
assume
A10: for X being non empty Subset of S holds f preserves_inf_of X;
now let X be non empty Subset of Sl;
reconsider Y = X as non empty Subset of S by A3;
f preserves_inf_of Y by A10;
hence g preserves_inf_of X by A3,WAYBEL_0:65;
end;
then g is continuous by WAYBEL19:8;
hence thesis by A1,A9,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
by WAYBEL_0:def 32;
hence thesis by Th45;
end;
definition
let S,T be non empty RelStr;
let f be map 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 = {"/\"({M.i where i is Element of M:i >= j},T)
where j is Element of M: not contradiction};
reconsider X = {"/\"
({N.i where i is Element of N:i >= j},S)
where j is Element of N: not contradiction}
as directed non empty Subset of S by Th25;
A2: ex_sup_of X,S & f preserves_sup_of X by A1,WAYBEL_0:def 37,YELLOW_0:17;
A3: the mapping of f*N = f*the mapping of N &
the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
A4: 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;
A5: f.:{INF(i) where i is Element of N: P[i]}
= {f.INF(i) where i is Element of N: P[i]}
from FuncFraenkel(A4);
A6: f.:X = Y
proof
A7: now let j be Element of N;
let j' be Element of M such that
A8: j' = j;
defpred Q[Element of N] means $1 >= j;
defpred Q'[Element of M] means $1 >= j';
deffunc F(Element of N) = f.(N.$1);
deffunc G(set) = f.((the mapping of N).$1);
A9: for v being Element of N st Q[v]
holds F(v) = G(v) by WAYBEL_0:def 8;
deffunc H(set) = (f*the mapping of N).$1;
deffunc I(Element of M) = M.$1;
A10: for v being Element of N st Q[v] holds G(v) = H(v)
by FUNCT_2:21;
A11: for v being Element of M st Q'[v] holds H(v) = I(v)
by A3,WAYBEL_0:def 8;
defpred P[set] means [j',$1] in the InternalRel of N;
A12: for v being Element of N
holds Q[v] iff P[v] by A8,ORDERS_1:def 9;
A13: for v being Element of M holds P[v] iff Q'[v]
by A3,ORDERS_1:def 9;
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 FuncFraenkel(A4)
.= {F(k) where k is Element of N: Q[k]}
.= {G(s) where s is Element of N: Q[s]}
from FraenkelF'R(A9)
.= {H(o) where o is Element of N: Q[o]}
from FraenkelF'R(A10)
.= {H(r) where r is Element of N: P[r]}
from Fraenkel6'(A12)
.= {H(m) where m is Element of M: P[m]} by A3
.= {H(q) where q is Element of M: Q'[q]}
from Fraenkel6'(A13)
.= {I(n) where n is Element of M: Q'[n]}
from FraenkelF'R(A11)
.= {M.n where n is Element of M: n >= j'};
end;
A14: now let j be Element of N;
A(j) c= the carrier of S
proof let b be set; 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;
f preserves_inf_of A & ex_inf_of A,S
by A1,WAYBEL_0:def 32,YELLOW_0:17;
hence f."/\"(A(j),S) = "/\"(f.:A(j), T) by WAYBEL_0:def 30;
end;
thus f.:X c= Y
proof let a be set; assume a in f.:X;
then consider j being Element of N such that
A15: a = f."/\"
({N.i where i is Element of N:i >= j},S) by A5;
A16: a = "/\"(f.:A(j),T) by A14,A15;
reconsider j' = j as Element of M by A3;
f.:A(j) = {M.n where n is Element of M: n >=
j'} by A7;
hence thesis by A16;
end;
let a be set; assume a in Y;
then consider j' being Element of M such that
A17: a = "/\"({M.n where n is Element of M: n >= j'},T);
reconsider j = j' as Element of N by A3;
a = "/\"(f.:A(j),T) by A7,A17 .= f."/\"(A(j),S) by A14;
hence thesis by A5;
end;
thus f.lim_inf N = f.sup X by WAYBEL11:def 6
.= sup (f.:X) by A2,WAYBEL_0:def 31
.= lim_inf (f*N) by A6,WAYBEL11:def 6;
end;
assume
A18: for N being net of S holds f.lim_inf N = lim_inf (f*N);
A19: f is directed-sups-preserving
proof let D be Subset of S; assume D is non empty directed;
then reconsider D' = 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 D' by WAYBEL17:10
.= lim_inf (f*Net-Str D') by A18
.= sup (f.:D) by Th33;
end;
A20: 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:25;
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 A18
.= inf fX by Th29
.= lim_inf (fX opp+id) by Th28;
hence thesis by Th28;
end;
end;
then f is infs-preserving by A20,WAYBEL_0:71;
hence f is continuous by A19,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 rng the mapping of N = Y by RELAT_1:71;
then A4: N is_eventually_in X by A2,Th27;
Lim N = {inf F} by WAYBEL19:43;
then {inf F} c= Cl X by A4,WAYBEL19:26;
then {inf F} c= X by A3,PRE_TOPC:52;
hence "/\"(Y, T) in the carrier of S by A2,ZFMISC_1:37;
end;
hence S is infs-inheriting 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 & the carrier of N = D by Th32;
then rng the mapping of N = Y by RELAT_1:71;
then N is_eventually_in X by A1,Th27;
then Lim N c= Cl X by WAYBEL19:26;
then A3: Lim N c= X by A2,PRE_TOPC:52;
sup D in Lim N by Th35;
hence "\/"(Y,T) in the carrier of S 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;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider X = the carrier of S as Subset of T;
take X; thus X = the carrier of S;
reconsider S as complete CLSubFrame of T by Th18;
consider SL being Lawson correct TopAugmentation of S;
A1: the RelStr of SL = the RelStr of S by YELLOW_9:def 4;
then A2: [#]SL = X by PRE_TOPC:12;
set f = incl(SL,T), f' = incl(S,T);
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then A3: f = id the carrier of SL & f' = id the carrier of SL
by A1,YELLOW_9:def 1;
A4: [#]SL is compact by COMPTS_1:10;
f' is infs-preserving & f' is directed-sups-preserving &
the RelStr of T = the RelStr of T by Th8,Th10;
then A5: f is infs-preserving directed-sups-preserving by A1,A3,Th6;
then f is SemilatticeHomomorphism of SL,T by Th5;
then f is continuous by A5,Th46;
then f.:[#]SL is compact by A4,WEIERSTR:14;
then X is compact by A2,A3,BORSUK_1:3;
hence X is closed by COMPTS_1:16;
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
A1: N.a in X & 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 = {"/\"(up(j), T)
where j is Element of N|a: not contradiction}
as directed non empty Subset of T by Th25;
iN c= X
proof let z be set; 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 set; assume u in up(j);
then consider i being Element of N|a such that
A3: u = (N|a).i & i >= j;
u = (the mapping of N|a).i & the carrier of N|a <> {}
by A3,WAYBEL_0:def 8;
then u in rng the mapping of N|a by FUNCT_2:6;
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;
jN is directed & ex_sup_of jN,T by WAYBEL10:24,YELLOW_0:17;
then "\/"(jN,T) in the carrier of S by WAYBEL_0:def 4;
then lim_inf (N|a) in X by WAYBEL11:def 6;
hence lim_inf N in X 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 by RELAT_1:71;
lim_inf (F opp+id) = inf F by Th28;
hence "/\"(Y, T) in the carrier of S by A2,A3;
end;
hence S is infs-inheriting 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 by RELAT_1:71;
lim_inf Net-Str F = sup F by WAYBEL17:10;
hence "\/"(Y, T) in the carrier of S 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 & 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,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
A2: for N being net of T st N is_eventually_in X holds lim_inf N in X;
now let N be net of T; assume
rng the mapping of N c= the carrier of S;
then N is_eventually_in X by A1,Th27;
hence lim_inf N in the carrier of S by A1,A2;
end;
then S is infs-inheriting directed-sups-inheriting by A1,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;