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;