:: Scott Topology :: by Andrzej Trybulec :: :: Received January 29, 1997 :: Copyright (c) 1997-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, TARSKI, REWRITE1, WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, EQREL_1, RELAT_2, FINSET_1, ORDINAL2, YELLOW_0, ZFMISC_1, STRUCT_0, CARD_1, RELAT_1, CARD_FIL, WAYBEL_9, RCOMP_1, NATTRA_1, PRE_TOPC, T_0TOPSP, CONNSP_2, TOPS_1, FUNCT_1, YELLOW_6, SEQM_3, CLASSES2, CLASSES1, YELLOW_2, PROB_1, WAYBEL_3, ORDINAL1, CARD_3, PBOOLE, WAYBEL_5, FUNCT_6, RLVECT_2, WAYBEL_6, RLVECT_3, YELLOW_8, WAYBEL11; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, DOMAIN_1, ORDINAL1, NUMBERS, STRUCT_0, WAYBEL_6, PRE_TOPC, TOPS_1, TOPS_2, CANTOR_1, CONNSP_2, T_0TOPSP, TDLAT_3, PBOOLE, CLASSES1, CLASSES2, CARD_3, PRALG_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_6, WAYBEL_9, YELLOW_8; constructors DOMAIN_1, CLASSES1, CLASSES2, TOPS_1, CONNSP_2, TDLAT_3, T_0TOPSP, CANTOR_1, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_9, YELLOW_8, RELSET_1, TOPS_2, WAYBEL_2, NUMBERS; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, TDLAT_3, WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_5, WAYBEL_9, RELSET_1, TOPS_1; requirements SUBSET, BOOLE, NUMERALS; definitions STRUCT_0, XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, YELLOW_0, RELAT_1, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3, TOPS_2, YELLOW_8, WAYBEL_6; equalities STRUCT_0, SUBSET_1, WAYBEL_0, YELLOW_6, WAYBEL_3, BINOP_1; expansions XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, YELLOW_0, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3; theorems TSP_1, WAYBEL_0, YELLOW_0, TARSKI, SUBSET_1, TOPS_1, YELLOW_2, SETFAM_1, CONNSP_2, ZFMISC_1, RELSET_1, TDLAT_3, TEX_1, ORDERS_2, LATTICE3, YELLOW_6, WAYBEL_5, DOMAIN_1, WAYBEL_7, YELLOW_1, YELLOW_3, WAYBEL_3, FUNCT_1, FUNCT_2, YELLOW_7, PRALG_1, WAYBEL_2, CLASSES1, RELAT_1, WAYBEL_4, YELLOW_8, XBOOLE_0, XBOOLE_1, PARTFUN1; schemes RELSET_1, DOMAIN_1, FRAENKEL, PBOOLE, XFAMILY; begin :: Preliminaries Lm1: for R,S being RelStr, p,q being Element of R, p9,q9 being Element of S st p = p9 & q = q9 & the RelStr of R = the RelStr of S holds p <= q implies p9 <= q9 proof let R,S be RelStr, p,q be Element of R, p9,q9 be Element of S such that A1: p = p9 and A2: q = q9 and A3: the RelStr of R = the RelStr of S; assume p <= q; then [p9,q9] in the InternalRel of S by A1,A2,A3,ORDERS_2:def 5; hence thesis by ORDERS_2:def 5; end; scheme Irrel{D,I() -> non empty set, P[set], F(set)->set, F(set,set)-> set}: { F(u) where u is Element of D(): P[u]} = { F(i,v) where i is Element of I(), v is Element of D(): P[v]} provided A1: for i being Element of I(), u being Element of D() holds F(u) = F(i,u) proof set A = { F(u) where u is Element of D(): P[u]}, B = { F(i,v) where i is Element of I(), v is Element of D(): P[v]}; thus A c= B proof let e be object; set i = the Element of I(); assume e in A; then consider u being Element of D() such that A2: e = F(u) and A3: P[u]; e = F(i,u) by A1,A2; hence thesis by A3; end; let e be object; assume e in B; then consider i being Element of I(), u being Element of D() such that A4: e = F(i,u) and A5: P[u]; e = F(u) by A1,A4; hence thesis by A5; end; theorem Th1: for L being complete LATTICE, X,Y being Subset of L st Y is_coarser_than X holds "/\"(X,L) <= "/\"(Y,L) proof let L be complete LATTICE, X,Y be Subset of L such that A1: Y is_coarser_than X; "/\"(X,L) is_<=_than Y proof let y be Element of L; assume y in Y; then consider x being Element of L such that A2: x in X and A3: x <= y by A1; "/\"(X,L) <= x by A2,YELLOW_2:22; hence "/\"(X,L) <= y by A3,YELLOW_0:def 2; end; hence thesis by YELLOW_0:33; end; theorem Th2: for L being complete LATTICE, X,Y being Subset of L st X is_finer_than Y holds "\/"(X,L) <= "\/"(Y,L) proof let L be complete LATTICE, X,Y be Subset of L such that A1: X is_finer_than Y; "\/"(Y,L) is_>=_than X proof let x be Element of L; assume x in X; then consider y being Element of L such that A2: y in Y and A3: x <= y by A1; "\/"(Y,L) >= y by A2,YELLOW_2:22; hence thesis by A3,YELLOW_0:def 2; end; hence thesis by YELLOW_0:32; end; theorem for T being RelStr, A being upper Subset of T, B being directed Subset of T holds A /\ B is directed proof let T be RelStr, A be upper Subset of T, B be directed Subset of T; let x,y be Element of T such that A1: x in A /\ B and A2: y in A /\ B; A3: x in B by A1,XBOOLE_0:def 4; y in B by A2,XBOOLE_0:def 4; then consider z being Element of T such that A4: z in B and A5: x <= z and A6: y <= z by A3,WAYBEL_0:def 1; take z; x in A by A1,XBOOLE_0:def 4; then z in A by A5,WAYBEL_0:def 20; hence z in A /\ B by A4,XBOOLE_0:def 4; thus thesis by A5,A6; end; registration let T be reflexive non empty RelStr; cluster non empty directed finite for Subset of T; existence proof set x = the Element of T; take {x}; thus thesis by WAYBEL_0:5; end; end; theorem Th4: :: uogolnione WAYBEL_3:16 for T being with_suprema Poset, D being non empty directed finite Subset of T holds sup D in D proof let T be reflexive transitive antisymmetric with_suprema RelStr, D be non empty directed finite Subset of T; D c= D; then reconsider E = D as finite Subset of D; consider x being Element of T such that A1: x in D and A2: x is_>=_than E by WAYBEL_0:1; A3: for b being Element of T st D is_<=_than b holds b >= x by A1; for c being Element of T st D is_<=_than c & for b being Element of T st D is_<=_than b holds b >= c holds c = x proof let c be Element of T such that A4: D is_<=_than c and A5: for b being Element of T st D is_<=_than b holds b >= c; A6: x >= c by A2,A5; c >= x by A1,A4; hence thesis by A6,ORDERS_2:2; end; then ex_sup_of D,T by A2,A3; hence thesis by A1,A2,A3,YELLOW_0:def 9; end; registration cluster reflexive transitive 1-element antisymmetric with_suprema with_infima finite strict for RelStr; existence proof 0 in {0} by TARSKI:def 1; then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3; reconsider T = RelStr(#{0},r#) as non empty RelStr; take T; thus T is reflexive proof let x be Element of T; x = 0 by TARSKI:def 1; then [x,x] in {[0,0]} by TARSKI:def 1; hence thesis by ORDERS_2:def 5; end; then reconsider T9 = T as 1-element reflexive RelStr; T9 is transitive; hence T is transitive; thus T is 1-element; T9 is antisymmetric; hence T is antisymmetric; T9 is with_suprema; hence T is with_suprema; T9 is with_infima; hence T is with_infima; thus T is finite; thus thesis; end; end; registration let T be finite 1-sorted; cluster -> finite for Subset of T; coherence; end; registration let R be RelStr; cluster empty -> lower upper for Subset of R; coherence; end; registration let R be 1-element RelStr; cluster -> upper for Subset of R; coherence proof let S be Subset of R; ex x being Element of R st ( the carrier of R = {x}) by TEX_1:def 1; then S = {}R or S = [#]R by ZFMISC_1:33; hence thesis; end; end; theorem Th5: for T being non empty RelStr, x being Element of T, A being upper Subset of T st not x in A holds A misses downarrow x proof let T be non empty RelStr, x be Element of T, A be upper Subset of T such that A1: not x in A; assume A meets downarrow x; then consider y being object such that A2: y in A and A3: y in downarrow x by XBOOLE_0:3; reconsider y as Element of T by A2; y <= x by A3,WAYBEL_0:17; hence contradiction by A1,A2,WAYBEL_0:def 20; end; theorem Th6: for T being non empty RelStr, x being Element of T, A being lower Subset of T st x in A holds downarrow x c= A proof let T be non empty RelStr, x be Element of T, A be lower Subset of T; assume x in A; then not x in A` by XBOOLE_0:def 5; then A` misses downarrow x by Th5; then A` c= (downarrow x)` by SUBSET_1:23; hence thesis by SUBSET_1:12; end; begin :: Scott Topology definition let T be non empty reflexive RelStr, S be Subset of T; attr S is inaccessible_by_directed_joins means :Def1: for D being non empty directed Subset of T st sup D in S holds D meets S; attr S is closed_under_directed_sups means :Def2: for D being non empty directed Subset of T st D c= S holds sup D in S; attr S is property(S) means :Def3: for D being non empty directed Subset of T st sup D in S ex y being Element of T st y in D & for x being Element of T st x in D & x >= y holds x in S; end; notation let T be non empty reflexive RelStr, S be Subset of T; synonym S is inaccessible for S is inaccessible_by_directed_joins; synonym S is directly_closed for S is closed_under_directed_sups; end; registration let T be non empty reflexive RelStr; cluster empty -> property(S) directly_closed for Subset of T; coherence; end; registration let T be non empty reflexive RelStr; cluster property(S) directly_closed for Subset of T; existence proof take {}T; thus thesis; end; end; registration let T be non empty reflexive RelStr, S be property(S) Subset of T; cluster S` -> directly_closed; coherence proof let D be non empty directed Subset of T such that A1: D c= S`; assume not sup D in S`; then sup D in S by XBOOLE_0:def 5; then consider y being Element of T such that A2: y in D and A3: for x being Element of T st x in D & x >= y holds x in S by Def3; y <= y; then y in S by A2,A3; then D /\ S <> {} by A2,XBOOLE_0:def 4; then D meets S; hence contradiction by A1,SUBSET_1:23; end; end; definition let T be reflexive non empty TopRelStr; attr T is Scott means :Def4: for S being Subset of T holds S is open iff S is inaccessible upper; end; registration let T be reflexive transitive antisymmetric non empty with_suprema finite RelStr; cluster -> inaccessible for Subset of T; coherence proof let S be Subset of T, D be non empty directed Subset of T such that A1: sup D in S; sup D in D by Th4; hence thesis by A1,XBOOLE_0:3; end; end; definition let T be reflexive transitive antisymmetric non empty with_suprema finite TopRelStr; redefine attr T is Scott means for S being Subset of T holds S is open iff S is upper; compatibility; end; registration cluster complete strict 1-element Scott for TopLattice; existence proof set T = the reflexive 1-element discrete strict finite TopRelStr; take T; thus T is complete strict 1-element; let S be Subset of T; thus thesis by TDLAT_3:15; end; end; registration let T be non empty reflexive RelStr; cluster [#]T -> directly_closed inaccessible; coherence proof thus [#]T is directly_closed; let D be non empty directed Subset of T such that sup D in [#]T; ex p being Element of T st ( p in D) by SUBSET_1:4; hence D meets [#]T by XBOOLE_0:3; end; end; registration let T be non empty reflexive RelStr; cluster directly_closed lower inaccessible upper for Subset of T; existence proof take [#]T; thus thesis; end; end; registration let T be non empty reflexive RelStr, S be inaccessible Subset of T; cluster S` -> directly_closed; coherence proof let D be non empty directed Subset of T; assume D c= S`; then D misses S by SUBSET_1:23; then not sup D in S by Def1; hence thesis by XBOOLE_0:def 5; end; end; registration let T be non empty reflexive RelStr, S be directly_closed Subset of T; cluster S` -> inaccessible; coherence proof let D be non empty directed Subset of T; assume sup D in S`; then not sup D in S by XBOOLE_0:def 5; then not D c= S`` by Def2; hence thesis by SUBSET_1:23; end; end; theorem Th7: :: p. 100, Remark 1.4 (i) for T being up-complete Scott non empty reflexive transitive TopRelStr, S being Subset of T holds S is closed iff S is directly_closed lower proof let T be up-complete Scott non empty reflexive transitive TopRelStr, S be Subset of T; hereby assume S is closed; then S` is open; then reconsider A = S` as inaccessible upper Subset of T by Def4; A` is directly_closed lower; hence S is directly_closed lower; end; assume S is directly_closed lower; then reconsider S as directly_closed lower Subset of T; S` is open by Def4; hence thesis; end; theorem Th8: for T being up-complete non empty reflexive transitive antisymmetric TopRelStr, x being Element of T holds downarrow x is directly_closed proof let T be up-complete non empty reflexive transitive antisymmetric TopRelStr, x be Element of T; downarrow x is directly_closed proof let D be non empty directed Subset of T; assume A1: D c= downarrow x; ex a being Element of T st a is_>=_than D & for b being Element of T st b is_>=_than D holds a <= b by WAYBEL_0:def 39; then A2: ex_sup_of D,T by YELLOW_0:15; x is_>=_than D by A1,WAYBEL_0:17; then sup D <= x by A2,YELLOW_0:30; hence thesis by WAYBEL_0:17; end; hence thesis; end; theorem Th9: :: p. 100, Remark 1.4 (ii) for T being complete Scott TopLattice, x being Element of T holds Cl {x} = downarrow x proof let T be complete Scott TopLattice, x be Element of T; downarrow x is directly_closed by Th8; then A1: downarrow x is closed by Th7; x <= x; then x in downarrow x by WAYBEL_0:17; then A2: {x} c= downarrow x by ZFMISC_1:31; now let C be Subset of T such that A3: {x} c= C; reconsider D = C as Subset of T; assume C is closed; then A4: D is lower by Th7; x in C by A3,ZFMISC_1:31; hence downarrow x c= C by A4,Th6; end; hence thesis by A1,A2,YELLOW_8:8; end; theorem :: p. 100, Remark 1.4 (iii) for T being complete Scott TopLattice holds T is T_0-TopSpace proof let T be complete Scott TopLattice; now let x,y be Point of T; reconsider x9 = x, y9 = y as Element of T; A1: Cl {x9} = downarrow x9 by Th9; A2: Cl {y9} = downarrow y9 by Th9; assume x <> y; hence Cl {x} <> Cl {y} by A1,A2,WAYBEL_0:19; end; hence thesis by TSP_1:def 5; end; theorem Th11: for T being Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, x being Element of T holds downarrow x is closed by Th8,Th7; theorem Th12: for T being up-complete Scott TopLattice, x being Element of T holds (downarrow x)` is open proof let T be up-complete Scott TopLattice, x be Element of T; downarrow x is closed by Th11; hence thesis; end; theorem Th13: for T being up-complete Scott TopLattice, x being Element of T, A being upper Subset of T st not x in A holds (downarrow x)` is a_neighborhood of A proof let T be up-complete Scott TopLattice, x be Element of T, A be upper Subset of T such that A1: not x in A; (downarrow x)` is open by Th12; then A2: Int (downarrow x)` = (downarrow x)` by TOPS_1:23; A misses downarrow x by A1,Th5; then A c= (downarrow x)` by SUBSET_1:23; hence thesis by A2,CONNSP_2:def 2; end; theorem :: p. 100, Remark 1.4 (iv) for T being complete Scott TopLattice, S being upper Subset of T ex F being Subset-Family of T st S = meet F & for X being Subset of T st X in F holds X is a_neighborhood of S proof let T be complete Scott TopLattice, S be upper Subset of T; defpred P[set] means $1 is a_neighborhood of S; set F = { X where X is Subset of T: P[X]}; F is Subset-Family of T from DOMAIN_1:sch 7; then reconsider F as Subset-Family of T; take F; thus S = meet F proof [#]T is a_neighborhood of S by CONNSP_2:28; then A1: [#]T in F; now let Z1 be set; assume Z1 in F; then ex X being Subset of T st Z1 = X & X is a_neighborhood of S; hence S c= Z1 by CONNSP_2:29; end; hence S c= meet F by A1,SETFAM_1:5; let x be object such that A2: x in meet F and A3: not x in S; reconsider p = x as Element of T by A2; (downarrow p)` is a_neighborhood of S by A3,Th13; then (downarrow p)` in F; then A4: meet F c= (downarrow p)` by SETFAM_1:3; p <= p; then p in downarrow p by WAYBEL_0:17; hence contradiction by A2,A4,XBOOLE_0:def 5; end; let X be Subset of T; assume X in F; then ex Y being Subset of T st X = Y & Y is a_neighborhood of S; hence thesis; end; theorem :: p. 100, Remark 1.4 (v) for T being Scott TopLattice, S being Subset of T holds S is open iff S is upper property(S) proof let T be Scott TopLattice, S be Subset of T; hereby assume A1: S is open; hence A2: S is upper by Def4; thus S is property(S) proof let D be non empty directed Subset of T such that A3: sup D in S; S is inaccessible by A1,Def4; then S meets D by A3; then consider y being object such that A4: y in S and A5: y in D by XBOOLE_0:3; reconsider y as Element of T by A4; take y; thus thesis by A2,A4,A5; end; end; assume that A6: S is upper and A7: S is property(S); S is inaccessible proof let D be non empty directed Subset of T; assume sup D in S; then consider y being Element of T such that A8: y in D and A9: for x being Element of T st x in D & x >= y holds x in S by A7; y >= y by YELLOW_0:def 1; then y in S by A8,A9; hence thesis by A8,XBOOLE_0:3; end; hence thesis by A6,Def4; end; registration let T be complete TopLattice; :: p. 100, Remark 1.4 (vi) cluster lower -> property(S) for Subset of T; coherence proof let S be Subset of T; assume A1: S is lower; let D be non empty directed Subset of T such that A2: sup D in S; consider y being Element of T such that A3: y in D by SUBSET_1:4; take y; thus y in D by A3; let x be Element of T such that A4: x in D and x >= y; x <= sup D by A4,YELLOW_2:22; hence thesis by A1,A2; end; end; Lm2: for T being non empty reflexive TopRelStr holds [#]T is property(S) proof let T be non empty reflexive TopRelStr; let D be non empty directed Subset of T such that sup D in [#]T; consider y being Element of T such that A1: y in D by SUBSET_1:4; take y; thus y in D by A1; let x be Element of T such that x in D and x >= y; thus thesis; end; theorem :: p. 100, Remark 1.4 (vii) for T being non empty transitive reflexive TopRelStr st the topology of T = { S where S is Subset of T: S is property(S)} holds T is TopSpace-like proof let T be non empty transitive reflexive TopRelStr such that A1: the topology of T = { S where S is Subset of T: S is property(S)}; [#]T is property(S) by Lm2; hence the carrier of T in the topology of T by A1; hereby let a be Subset-Family of T such that A2: a c= the topology of T; union a is property(S) proof let D be non empty directed Subset of T; assume sup D in union a; then consider x being set such that A3: sup D in x and A4: x in a by TARSKI:def 4; x in the topology of T by A2,A4; then consider X being Subset of T such that A5: x = X and A6: X is property(S) by A1; consider y being Element of T such that A7: y in D and A8: for x being Element of T st x in D & x >= y holds x in X by A3,A5,A6; take y; thus y in D by A7; let u be Element of T; assume that A9: u in D and A10: u >= y; u in X by A8,A9,A10; hence thesis by A4,A5,TARSKI:def 4; end; hence union a in the topology of T by A1; end; let a,b be Subset of T; assume a in the topology of T; then consider A being Subset of T such that A11: a = A and A12: A is property(S) by A1; assume b in the topology of T; then consider B being Subset of T such that A13: b = B and A14: B is property(S) by A1; A /\ B is property(S) proof let D be non empty directed Subset of T; assume A15: sup D in A /\ B; then sup D in A by XBOOLE_0:def 4; then consider x being Element of T such that A16: x in D and A17: for z being Element of T st z in D & z >= x holds z in A by A12; sup D in B by A15,XBOOLE_0:def 4; then consider y being Element of T such that A18: y in D and A19: for z being Element of T st z in D & z >= y holds z in B by A14; consider z being Element of T such that A20: z in D and A21: x <= z and A22: y <= z by A16,A18,WAYBEL_0:def 1; take z; thus z in D by A20; let u be Element of T such that A23: u in D; assume A24: u >= z; then u >= x by A21,YELLOW_0:def 2; then A25: u in A by A17,A23; u >= y by A22,A24,YELLOW_0:def 2; then u in B by A19,A23; hence thesis by A25,XBOOLE_0:def 4; end; hence thesis by A1,A11,A13; end; begin :: Scott Convergence reserve R for non empty RelStr, N for net of R, i for Element of N; definition let R,N; func lim_inf N -> Element of R equals "\/"((the set of all "/\"({N.i:i >= j},R) where j is Element of N),R); correctness; end; definition let R be reflexive non empty RelStr; let N be net of R, p be Element of R; pred p is_S-limit_of N means p <= lim_inf N; end; definition let R be reflexive non empty RelStr; func Scott-Convergence R -> Convergence-Class of R means :Def8: for N being strict net of R st N in NetUniv R for p being Element of R holds [N,p] in it iff p is_S-limit_of N; existence proof defpred P[set,Element of R] means ex N being strict net of R st N = $1 & $2 is_S-limit_of N; consider C being Relation of NetUniv R, the carrier of R such that A1: for x being Element of NetUniv R, y being Element of R holds [x,y] in C iff P[x,y] from RELSET_1:sch 2; reconsider C as Convergence-Class of R by YELLOW_6:def 18; take C; let N be strict net of R such that A2: N in NetUniv R; let p be Element of R; hereby assume [N,p] in C; then ex M being strict net of R st M = N & p is_S-limit_of M by A1,A2; hence p is_S-limit_of N; end; thus thesis by A1,A2; end; uniqueness proof let it1,it2 be Convergence-Class of R such that A3: for N being strict net of R st N in NetUniv R for p being Element of R holds [N,p] in it1 iff p is_S-limit_of N and A4: for N being strict net of R st N in NetUniv R for p being Element of R holds [N,p] in it2 iff p is_S-limit_of N; let x,y be object; A5: it1 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18; A6: it2 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18; hereby assume A7: [x,y] in it1; then A8: x in NetUniv R by A5,ZFMISC_1:87; then consider N being strict net of R such that A9: N = x and the carrier of N in the_universe_of the carrier of R by YELLOW_6:def 11; reconsider p = y as Element of R by A5,A7,ZFMISC_1:87; p is_S-limit_of N by A3,A7,A8,A9; hence [x,y] in it2 by A4,A8,A9; end; assume A10: [x,y] in it2; then A11: x in NetUniv R by A6,ZFMISC_1:87; then consider N being strict net of R such that A12: N = x and the carrier of N in the_universe_of the carrier of R by YELLOW_6:def 11; reconsider p = y as Element of R by A6,A10,ZFMISC_1:87; p is_S-limit_of N by A4,A10,A11,A12; hence thesis by A3,A11,A12; end; end; :: remarks, p.98 theorem for R being complete LATTICE, N being net of R, p,q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds p <= q proof let R be complete LATTICE, N be net of R, p,q be Element of R such that A1: p <= lim_inf N and A2: N is_eventually_in downarrow q; consider j0 being Element of N such that A3: for i being Element of N st j0 <= i holds N.i in downarrow q by A2; set X = the set of all "/\"({N.i where i is Element of N: i >= j},R) where j is Element of N; reconsider q9= q as Element of R; q9 is_>=_than X proof let x be Element of R; assume x in X; then consider j1 being Element of N such that A4: x = "/\"({N.i where i is Element of N: i >= j1},R); set Y = {N.i where i is Element of N: i >= j1}; reconsider j1 as Element of N; consider j2 being Element of N such that A5: j2 >= j0 and A6: j2 >= j1 by YELLOW_6:def 3; N.j2 in Y by A6; then A7: x <= N.j2 by A4,YELLOW_2:22; N.j2 in downarrow q by A3,A5; then N.j2 <= q9 by WAYBEL_0:17; hence x <= q9 by A7,YELLOW_0:def 2; end; then lim_inf N <= q9 by YELLOW_0:32; hence thesis by A1,YELLOW_0:def 2; end; theorem Th18: for R being complete LATTICE, N being net of R, p,q being Element of R st N is_eventually_in uparrow q holds lim_inf N >= q proof let R be complete LATTICE, N be net of R, p,q be Element of R; assume N is_eventually_in uparrow q; then consider j0 being Element of N such that A1: for i being Element of N st j0 <= i holds N.i in uparrow q; set X = the set of all "/\"({N.i where i is Element of N: i >= j},R) where j is Element of N; set Y = {N.i where i is Element of N: i >= j0}; reconsider q9= q as Element of R; "/\"(Y,R) in X; then A2: lim_inf N >= "/\"(Y,R) by YELLOW_2:22; q9 is_<=_than Y proof let y be Element of R; assume y in Y; then consider i1 being Element of N such that A3: y = N.i1 and A4: i1 >= j0; reconsider i19 = i1 as Element of N; N.i19 in uparrow q by A1,A4; hence q9 <= y by A3,WAYBEL_0:18; end; then "/\"(Y,R) >= q9 by YELLOW_0:33; hence thesis by A2,YELLOW_0:def 2; end; definition let R be reflexive non empty RelStr, N be non empty NetStr over R; redefine attr N is monotone means :Def9: for i,j being Element of N st i <= j holds N.i <= N.j; compatibility proof hereby assume N is monotone; then A1: netmap(N,R) is monotone; let i,j be Element of N; assume i <= j; hence N.i <= N.j by A1; end; assume A2: for i,j being Element of N st i <= j holds N.i <= N.j; netmap(N,R) is monotone proof let x,y be Element of N; A3: netmap(N,R).x = N.x; A4: netmap(N,R).y = N.y; assume x <= y; hence netmap(N,R).x <= netmap(N,R).y by A2,A3,A4; end; hence thesis; end; end; definition let R be non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; func Net-Str(S,f) -> strict non empty NetStr over R means :Def10: the carrier of it = S & the mapping of it = f & for i,j being Element of it holds i <= j iff it.i <= it.j; existence proof defpred P[Element of S, Element of S] means f.$1 <= f.$2; consider R being Relation of S,S such that A1: for x,y being Element of S holds [x,y] in R iff P[x,y] from RELSET_1:sch 2; take N = NetStr(#S,R,f#); thus the carrier of N = S; thus the mapping of N = f; let i,j be Element of N; reconsider x = i, y = j as Element of S; [x,y] in the InternalRel of N iff f.x <= f.y by A1; hence thesis by ORDERS_2:def 5; end; uniqueness proof let it1,it2 be strict non empty NetStr over R such that A2: the carrier of it1 = S and A3: the mapping of it1 = f and A4: for i,j being Element of it1 holds i <= j iff it1.i <= it1.j and A5: the carrier of it2 = S and A6: the mapping of it2 = f and A7: for i,j being Element of it2 holds i <= j iff it2.i <= it2.j; the InternalRel of it1 = the InternalRel of it2 proof let x,y be object; hereby assume A8: [x,y] in the InternalRel of it1; then reconsider i=x, j=y as Element of it1 by ZFMISC_1:87; reconsider i9=x, j9=y as Element of it2 by A2,A5,A8,ZFMISC_1:87; A9: it1.i = it2.i9 by A3,A6; A10: it1.j = it2.j9 by A3,A6; i <= j by A8,ORDERS_2:def 5; then it2.i9 <= it2.j9 by A4,A9,A10; then i9 <= j9 by A7; hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5; end; assume A11: [x,y] in the InternalRel of it2; then reconsider i=x, j=y as Element of it2 by ZFMISC_1:87; reconsider i9=x, j9=y as Element of it1 by A2,A5,A11,ZFMISC_1:87; A12: it2.i = it1.i9 by A3,A6; A13: it2.j = it1.j9 by A3,A6; i <= j by A11,ORDERS_2:def 5; then it1.i9 <= it1.j9 by A7,A12,A13; then i9 <= j9 by A4; hence thesis by ORDERS_2:def 5; end; hence thesis by A2,A3,A5,A6; end; end; theorem Th19: for L being non empty 1-sorted, N being non empty NetStr over L holds rng the mapping of N = the set of all N.i where i is Element of N proof let L be non empty 1-sorted, N be non empty NetStr over L; set X = the set of all N.i where i is Element of N; A1: the carrier of N = dom the mapping of N by FUNCT_2:def 1; thus rng the mapping of N c= the set of all N.i where i is Element of N proof let e be object; assume e in rng the mapping of N; then consider u being object such that A2: u in dom the mapping of N and A3: e = (the mapping of N).u by FUNCT_1:def 3; reconsider u as Element of N by A2; e = N.u by A3; hence thesis; end; let e be object; assume e in X; then ex i being Element of N st ( e = N.i); hence thesis by A1,FUNCT_1:def 3; end; theorem Th20: for R being non empty RelStr, S being non empty set, f be Function of S, the carrier of R st rng f is directed holds Net-Str(S,f) is directed proof let R be non empty RelStr, S be non empty set, f be Function of S, the carrier of R such that A1: rng f is directed; set N = Net-Str(S,f); let x,y be Element of N; f = the mapping of N by Def10; then A2: rng f = the set of all N.i where i is Element of N by Th19; then A3: N.x in rng f; N.y in rng f by A2; then consider p being Element of R such that A4: p in rng f and A5: N.x <= p and A6: N.y <= p by A1,A3; consider z being object such that A7: z in dom f and A8: p = f.z by A4,FUNCT_1:def 3; reconsider z as Element of N by A7,Def10; take z; p = N.z by A8,Def10; hence thesis by A5,A6,Def10; end; registration let R be non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; cluster Net-Str(S,f) -> monotone; coherence proof set N = Net-Str(S,f); netmap(N,R) is monotone proof let x,y be Element of N; A1: netmap(N,R).x = N.x; A2: netmap(N,R).y = N.y; assume x <= y; hence netmap(N,R).x <= netmap(N,R).y by A1,A2,Def10; end; hence thesis; end; end; registration let R be transitive non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; cluster Net-Str(S,f) -> transitive; coherence proof set N = Net-Str(S,f); let x,y,z be Element of N; assume that A1: x <= y and A2: y <= z; A3: N.x <= N.y by A1,Def10; N.y <= N.z by A2,Def10; then N.x <= N.z by A3,YELLOW_0:def 2; hence thesis by Def10; end; end; registration let R be reflexive non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; cluster Net-Str(S,f) -> reflexive; coherence proof let x be Element of Net-Str(S,f); Net-Str(S,f).x <= Net-Str(S,f).x; hence thesis by Def10; end; end; theorem Th21: for R being non empty transitive RelStr, S being non empty set, f be Function of S, the carrier of R st S c= the carrier of R & Net-Str(S,f) is directed holds Net-Str(S,f) in NetUniv R proof let R be non empty transitive RelStr, S be non empty set, f be Function of S, the carrier of R such that A1: S c= the carrier of R and A2: Net-Str(S,f) is directed; reconsider N = Net-Str(S,f) as strict net of R by A2; set UN = the_universe_of the carrier of R; reconsider UN as universal set; the_transitive-closure_of the carrier of R in UN by CLASSES1:2; then the carrier of R in UN by CLASSES1:3,52; then A3: S in UN by A1,CLASSES1:def 1; the carrier of N = S by Def10; hence thesis by A3,YELLOW_6:def 11; end; registration let R be LATTICE; cluster monotone reflexive strict for net of R; existence proof reconsider f = id the carrier of R as Function of the carrier of R, the carrier of R; rng f = [#]R by RELAT_1:45; then reconsider N = Net-Str(the carrier of R,f) as strict reflexive net of R by Th20; take N; thus thesis; end; end; defpred P[set] means not contradiction; theorem Th22: for R being complete LATTICE, N being monotone reflexive net of R holds lim_inf N = sup N proof let R be complete LATTICE, N be monotone reflexive net of R; deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R); set X = {F(j) where j is Element of N: P[j]}; deffunc G(Element of N) = N.$1; A1: for j being Element of N holds G(j) = F(j) proof let j be Element of N; set Y = {N.i where i is Element of N: i >= j}; A2: N.j is_<=_than Y proof let y be Element of R; assume y in Y; then ex i being Element of N st y = N.i & j <= i; hence N.j <= y by Def9; end; for b being Element of R st b is_<=_than Y holds N.j >= b proof let b be Element of R; assume A3: b is_<=_than Y; reconsider j9 = j as Element of N; j9 <= j9; then N.j9 in Y; hence thesis by A3; end; hence thesis by A2,YELLOW_0:33; end; rng the mapping of N = { G(j) where j is Element of N: P[j]} by Th19 .= X from FRAENKEL:sch 5(A1); hence lim_inf N = Sup the mapping of N by YELLOW_2:def 5 .= sup N by WAYBEL_2:def 1; end; theorem Th23: for R being complete LATTICE, N being constant net of R holds the_value_of N = lim_inf N proof let R be complete LATTICE, N be constant net of R; set X = the set of all "/\"({N.i where i is Element of N: i >= j},R) where j is Element of N; set j = the Element of N; A1: N.j is_>=_than X proof let b be Element of R; assume b in X; then consider j0 being Element of N such that A2: b = "/\"({N.i where i is Element of N: i >= j0},R); reconsider j0 as Element of N; consider i0 being Element of N such that A3: i0 >= j0 and i0 >= j0 by YELLOW_6:def 3; A4: N.i0 in {N.i where i is Element of N: i >= j0} by A3; N.i0 = the_value_of N by YELLOW_6:16 .= N.j by YELLOW_6:16; hence thesis by A2,A4,YELLOW_2:22; end; A5: for b being Element of R st b is_>=_than X holds N.j <= b proof let b be Element of R; set Y = {N.i where i is Element of N: i >= j}; A6: "/\"(Y,R) in X; assume b is_>=_than X; then A7: b >= "/\"(Y,R) by A6; A8: N.j is_<=_than Y proof let c be Element of R; assume c in Y; then consider i0 being Element of N such that A9: c = N.i0 and i0 >= j; N.j = the_value_of N by YELLOW_6:16 .= N.i0 by YELLOW_6:16; hence N.j <= c by A9; end; for b being Element of R st b is_<=_than Y holds N.j >= b proof let c be Element of R; consider i0 being Element of N such that A10: i0 >= j and i0 >= j by YELLOW_6:def 3; A11: N.i0 in Y by A10; assume A12: c is_<=_than Y; N.j = the_value_of N by YELLOW_6:16 .= N.i0 by YELLOW_6:16; hence thesis by A11,A12; end; hence thesis by A7,A8,YELLOW_0:33; end; thus the_value_of N = N.j by YELLOW_6:16 .= lim_inf N by A1,A5,YELLOW_0:32; end; theorem Th24: for R being complete LATTICE, N being constant net of R holds the_value_of N is_S-limit_of N by Th23; definition let S be non empty 1-sorted, e be Element of S; func Net-Str e -> strict NetStr over S means :Def11: the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e}; existence proof e in {e} by TARSKI:def 1; then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3; A1: dom id{e} = {e} by RELAT_1:45; rng id{e} = {e} by RELAT_1:45; then reconsider f = id{e} as Function of {e}, the carrier of S by A1,RELSET_1:4; take NetStr(#{e},r,f#); thus thesis; end; uniqueness; end; registration let S be non empty 1-sorted, e be Element of S; cluster Net-Str e -> non empty; coherence proof set N = Net-Str e; the carrier of N = {e} by Def11; hence the carrier of N is non empty; end; end; theorem Th25: for S being non empty 1-sorted, e being Element of S, x being Element of Net-Str e holds x = e proof let S be non empty 1-sorted, e be Element of S, x be Element of Net-Str e; the carrier of Net-Str e = {e} by Def11; hence thesis by TARSKI:def 1; end; theorem Th26: for S being non empty 1-sorted, e being Element of S, x being Element of Net-Str e holds (Net-Str e).x = e proof let S be non empty 1-sorted, e be Element of S, x be Element of Net-Str e; set N = Net-Str e; A1: the carrier of Net-Str e = {e} by Def11; then A2: x = e by TARSKI:def 1; thus N.x = (id{e}).x by Def11 .= e by A1,A2; end; registration let S be non empty 1-sorted, e be Element of S; cluster Net-Str e -> reflexive transitive directed antisymmetric; coherence proof set N = Net-Str e; the carrier of N = {e} by Def11; then reconsider e as Element of N by TARSKI:def 1; the InternalRel of N = {[e,e]} by Def11; then A1: [e,e] in the InternalRel of N by TARSKI:def 1; thus N is reflexive proof let x be Element of N; x = e by Th25; hence thesis by A1,ORDERS_2:def 5; end; thus N is transitive proof let x,y,z be Element of N such that x <= y and y <= z; A2: x = e by Th25; z = e by Th25; hence thesis by A1,A2,ORDERS_2:def 5; end; thus N is directed proof let x,y be Element of N; take e; A3: x = e by Th25; y = e by Th25; hence thesis by A1,A3,ORDERS_2:def 5; end; let x,y be Element of N such that x <= y and y <= x; x = e by Th25; hence thesis by Th25; end; end; theorem Th27: for S being non empty 1-sorted, e being Element of S, X being set holds Net-Str e is_eventually_in X iff e in X proof let S be non empty 1-sorted, e be Element of S, X be set; set N = Net-Str e; the carrier of N = {e} by Def11; then reconsider d = e as Element of N by TARSKI:def 1; hereby assume N is_eventually_in X; then consider x being Element of N such that A1: for y being Element of N st x <= y holds N.y in X; N.x in X by A1; hence e in X by Th26; end; assume A2: e in X; take d; let j be Element of N such that d <= j; thus thesis by A2,Th26; end; theorem Th28: for S being reflexive antisymmetric non empty RelStr, e being Element of S holds e = lim_inf Net-Str e proof let S be reflexive antisymmetric non empty RelStr, e be Element of S; set N = Net-Str e, X = the set of all "/\"({N.i where i is Element of N: i >= j},S) where j is Element of N; reconsider e9 = e as Element of S; A1: X c= {e9} proof let u be object; assume u in X; then consider j being Element of N such that A2: u = "/\"({N.i where i is Element of N: i >= j},S); set Y = {N.i where i is Element of N: i >= j}; A3: Y c= {e9} proof let v be object; assume v in Y; then consider i being Element of N such that A4: v = N.i and i >= j; reconsider i9 = i as Element of N; N.i9 = e by Th26; hence thesis by A4,TARSKI:def 1; end; reconsider j9 = j as Element of N; j9 <= j9; then N.j in Y; then Y = {e9} by A3,ZFMISC_1:33; then u = e9 by A2,YELLOW_0:39; hence thesis by TARSKI:def 1; end; set j = the Element of N; "/\"({N.i where i is Element of N: i >= j},S) in X; then X = {e9} by A1,ZFMISC_1:33; hence thesis by YELLOW_0:39; end; theorem Th29: for S being non empty reflexive RelStr, e being Element of S holds Net-Str e in NetUniv S proof let S be non empty reflexive RelStr, e be Element of S; set N = Net-Str e, UN = the_universe_of the carrier of S; A1: the carrier of N = {e} by Def11; reconsider UN as universal set; the_transitive-closure_of the carrier of S in UN by CLASSES1:2; then the carrier of S in UN by CLASSES1:3,52; then the carrier of N in the_universe_of the carrier of S by A1, CLASSES1:def 1; hence thesis by YELLOW_6:def 11; end; theorem Th30: for R being complete LATTICE, Z be net of R, D be Subset of R st D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R) where j is Element of Z holds D is non empty directed proof let R be complete LATTICE, Z be net of R, D be Subset of R; assume A1: D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R) where j is Element of Z; set j = the Element of Z; "/\"({Z.k where k is Element of Z: k >= j},R) in D by A1; hence D is non empty; let x,y be Element of R; assume x in D; then consider jx being Element of Z such that A2: x = "/\"({Z.k where k is Element of Z: k >= jx},R) by A1; assume y in D; then consider jy being Element of Z such that A3: y = "/\"({Z.k where k is Element of Z: k >= jy},R) by A1; reconsider jx, jy as Element of Z; consider j being Element of Z such that A4: j >= jx and A5: j >= jy by YELLOW_6:def 3; set E1 = {Z.k where k is Element of Z: k >= jx}, Ey = {Z.k where k is Element of Z: k >= jy}, E = {Z.k where k is Element of Z: k >= j}; take z = "/\"({Z.k where k is Element of Z: k >= j},R); thus z in D by A1; E c= E1 proof let e be object; assume e in E; then consider k being Element of Z such that A6: e = Z.k and A7: k >= j; reconsider k as Element of Z; k >= jx by A4,A7,YELLOW_0:def 2; hence thesis by A6; end; hence x <= z by A2,WAYBEL_7:1; E c= Ey proof let e be object; assume e in E; then consider k being Element of Z such that A8: e = Z.k and A9: k >= j; reconsider k as Element of Z; k >= jy by A5,A9,YELLOW_0:def 2; hence thesis by A8; end; hence y <= z by A3,WAYBEL_7:1; end; theorem Th31: :: 1.2. Lemma, p.99 for L being complete LATTICE for S being Subset of L holds S in the topology of ConvergenceSpace Scott-Convergence L iff S is inaccessible upper proof let L be complete LATTICE; set SC = Scott-Convergence L, T = ConvergenceSpace SC; A1: the topology of T = { V where V is Subset of L: for p being Element of L st p in V for N being net of L st [N,p] in SC holds N is_eventually_in V} by YELLOW_6:def 24; let S be Subset of L; hereby assume S in the topology of T; then A2: ex V being Subset of L st ( S = V)&( for p being Element of L st p in V for N being net of L st [N,p] in SC holds N is_eventually_in V) by A1; thus S is inaccessible proof let D be non empty directed Subset of L such that A3: sup D in S; A4: dom id D = D by RELAT_1:45; A5: rng id D = D by RELAT_1:45; then reconsider f = id D as Function of D, the carrier of L by A4,RELSET_1:4; reconsider N = Net-Str(D,f) as strict monotone reflexive net of L by A5,Th20; A6: N in NetUniv L by Th21; lim_inf N = sup N by Th22 .= Sup the mapping of N by WAYBEL_2:def 1 .= "\/"(rng the mapping of N,L) by YELLOW_2:def 5 .= "\/"(rng f,L) by Def10 .= sup D by RELAT_1:45; then sup D is_S-limit_of N; then [N,sup D] in SC by A6,Def8; then N is_eventually_in S by A2,A3; then consider i0 being Element of N such that A7: for j being Element of N st i0 <= j holds N.j in S; consider j0 being Element of N such that A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def 3; A9: N.j0 in S by A7,A8; A10: D = the carrier of N by Def10; N.j0 = (id D).j0 by Def10 .= j0 by A10; hence thesis by A9,A10,XBOOLE_0:3; end; thus S is upper proof let x,y be Element of L such that A11: x in S and A12: x <= y; A13: Net-Str y in NetUniv L by Th29; y = lim_inf Net-Str y by Th28; then x is_S-limit_of Net-Str y by A12; then [Net-Str y,x] in SC by A13,Def8; then Net-Str y is_eventually_in S by A2,A11; hence thesis by Th27; end; end; assume that A14: S is inaccessible and A15: S is upper; for p being Element of L st p in S for N being net of L st [N,p] in SC holds N is_eventually_in S proof let p be Element of L such that A16: p in S; reconsider p9 = p as Element of L; let N be net of L; assume A17: [N,p] in SC; SC c= [:NetUniv L, the carrier of L:] by YELLOW_6:def 18; then A18: N in NetUniv L by A17,ZFMISC_1:87; then ex N9 being strict net of L st N9 = N & the carrier of N9 in the_universe_of the carrier of L by YELLOW_6:def 11; then p is_S-limit_of N by A17,A18,Def8; then A19: p9 <= lim_inf N; deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},L); set X ={F(j) where j is Element of N: P[j]}; X is Subset of L from DOMAIN_1:sch 8; then reconsider D = X as Subset of L; reconsider D as non empty directed Subset of L by Th30; sup D in S by A15,A16,A19; then D meets S by A14; then D /\ S <> {}; then consider d being Element of L such that A20: d in D /\ S by SUBSET_1:4; reconsider d as Element of L; d in D by A20,XBOOLE_0:def 4; then consider j being Element of N such that A21: d = "/\"({N.i where i is Element of N: i >= j},L); reconsider j as Element of N; take j; let i0 be Element of N; A22: d in S by A20,XBOOLE_0:def 4; assume j <= i0; then N.i0 in {N.i where i is Element of N: i >= j}; then d <= N.i0 by A21,YELLOW_2:22; hence thesis by A15,A22; end; hence thesis by A1; end; theorem Th32: for T being complete Scott TopLattice holds the TopStruct of T = ConvergenceSpace Scott-Convergence T proof let T be complete Scott TopLattice; set CSC = ConvergenceSpace Scott-Convergence T; the topology of T = the topology of CSC proof thus the topology of T c= the topology of CSC proof let e be object; assume A1: e in the topology of T; then reconsider A = e as Subset of T; A is open by A1; then A is inaccessible upper by Def4; hence thesis by Th31; end; let e be object; assume A2: e in the topology of CSC; then reconsider A = e as Subset of T by YELLOW_6:def 24; A is inaccessible upper by A2,Th31; then A is open by Def4; hence thesis; end; hence thesis by YELLOW_6:def 24; end; theorem Th33: for T being complete TopLattice st the TopStruct of T = ConvergenceSpace Scott-Convergence T for S being Subset of T holds S is open iff S is inaccessible upper proof let T be complete TopLattice; set SC = Scott-Convergence T; assume the TopStruct of T = ConvergenceSpace SC; then A1: the topology of T = { V where V is Subset of T: for p being Element of T st p in V for N being net of T st [N,p] in SC holds N is_eventually_in V} by YELLOW_6:def 24; let S be Subset of T; hereby assume S is open; then S in the topology of T; then A2: ex V being Subset of T st ( S = V)&( for p being Element of T st p in V for N being net of T st [N,p] in SC holds N is_eventually_in V) by A1; thus S is inaccessible proof let D be non empty directed Subset of T such that A3: sup D in S; A4: dom id D = D by RELAT_1:45; A5: rng id D = D by RELAT_1:45; then reconsider f = id D as Function of D, the carrier of T by A4,RELSET_1:4; reconsider N = Net-Str(D,f) as strict monotone reflexive net of T by A5,Th20; A6: N in NetUniv T by Th21; lim_inf N = sup N by Th22 .= Sup the mapping of N by WAYBEL_2:def 1 .= "\/"(rng the mapping of N,T) by YELLOW_2:def 5 .= "\/"(rng f,T) by Def10 .= sup D by RELAT_1:45; then sup D is_S-limit_of N; then [N,sup D] in SC by A6,Def8; then N is_eventually_in S by A2,A3; then consider i0 being Element of N such that A7: for j being Element of N st i0 <= j holds N.j in S; consider j0 being Element of N such that A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def 3; A9: N.j0 in S by A7,A8; A10: D = the carrier of N by Def10; N.j0 = (id D).j0 by Def10 .= j0 by A10; hence thesis by A9,A10,XBOOLE_0:3; end; thus S is upper proof let x,y be Element of T such that A11: x in S and A12: x <= y; A13: Net-Str y in NetUniv T by Th29; y = lim_inf Net-Str y by Th28; then x is_S-limit_of Net-Str y by A12; then [Net-Str y,x] in SC by A13,Def8; then Net-Str y is_eventually_in S by A2,A11; hence thesis by Th27; end; end; assume that A14: S is inaccessible and A15: S is upper; for p being Element of T st p in S for N being net of T st [N,p] in SC holds N is_eventually_in S proof let p be Element of T such that A16: p in S; reconsider p9 = p as Element of T; let N be net of T; assume A17: [N,p] in SC; SC c= [:NetUniv T, the carrier of T:] by YELLOW_6:def 18; then A18: N in NetUniv T by A17,ZFMISC_1:87; then ex N9 being strict net of T st N9 = N & the carrier of N9 in the_universe_of the carrier of T by YELLOW_6:def 11; then p is_S-limit_of N by A17,A18,Def8; then A19: p9 <= lim_inf N; deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},T); set X ={F(j) where j is Element of N: P[j]}; X is Subset of T from DOMAIN_1:sch 8; then reconsider D = X as Subset of T; reconsider D as non empty directed Subset of T by Th30; sup D in S by A15,A16,A19; then D meets S by A14; then D /\ S <> {}; then consider d being Element of T such that A20: d in D /\ S by SUBSET_1:4; reconsider d as Element of T; d in D by A20,XBOOLE_0:def 4; then consider j being Element of N such that A21: d = "/\"({N.i where i is Element of N: i >= j},T); reconsider j as Element of N; take j; let i0 be Element of N; A22: d in S by A20,XBOOLE_0:def 4; assume j <= i0; then N.i0 in {N.i where i is Element of N: i >= j}; then d <= N.i0 by A21,YELLOW_2:22; hence thesis by A15,A22; end; then S in the topology of T by A1; hence thesis; end; theorem Th34: for T being complete TopLattice st the TopStruct of T = ConvergenceSpace Scott-Convergence T holds T is Scott by Th33; registration let R be complete LATTICE; :: 1.6. Proposition (i) cluster Scott-Convergence R -> (CONSTANTS); coherence proof let N be constant net of R; assume A1: N in NetUniv R; then consider M being strict net of R such that A2: M = N and the carrier of M in the_universe_of the carrier of R by YELLOW_6:def 11; the_value_of M is_S-limit_of M by A2,Th24; hence thesis by A1,A2,Def8; end; end; registration let R be complete LATTICE; :: 1.6. Proposition (i) cluster Scott-Convergence R -> (SUBNETS); coherence proof set S = Scott-Convergence R; let N be net of R, Y be subnet of N; A1: S c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18; assume A2: Y in NetUniv R; then consider Y9 being strict net of R such that A3: Y9 = Y and the carrier of Y9 in the_universe_of the carrier of R by YELLOW_6:def 11; let p be Element of R; assume A4: [N,p] in S; then A5: N in NetUniv R by A1,ZFMISC_1:87; then consider N9 being strict net of R such that A6: N9 = N and the carrier of N9 in the_universe_of the carrier of R by YELLOW_6:def 11; deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R); reconsider X1 = {F(j) where j is Element of N: P[j]} as Subset of R from DOMAIN_1:sch 8; deffunc G(Element of Y) = "/\"({Y.i where i is Element of Y: i >= $1},R); reconsider X2 = {G(j) where j is Element of Y: P[j]} as Subset of R from DOMAIN_1:sch 8; p is_S-limit_of N9 by A4,A5,A6,Def8; then A7: p <= lim_inf N by A6; consider f being Function of Y, N such that A8: the mapping of Y = (the mapping of N)*f and A9: for m being Element of N ex n being Element of Y st for p being Element of Y st n <= p holds m <= f.p by YELLOW_6:def 9; X1 is_finer_than X2 proof let a be Element of R; assume a in X1; then consider j being Element of N such that A10: a = "/\"({N.i where i is Element of N: i >= j},R); reconsider j as Element of N; consider n being Element of Y such that A11: for p being Element of Y st n <= p holds j <= f.p by A9; set X3 = {Y.i where i is Element of Y: i >= n}, X4 = {N.i where i is Element of N: i >= j}; take b = "/\"(X3,R); thus b in X2; X3 c= X4 proof let u be object; assume u in X3; then consider m being Element of Y such that A12: u = Y.m and A13: m >= n; reconsider m as Element of Y; A14: f.m >= j by A11,A13; u = N.(f.m) by A8,A12,FUNCT_2:15; hence thesis by A14; end; hence a <= b by A10,WAYBEL_7:1; end; then "\/"(X1,R) <= "\/"(X2,R) by Th2; then p <= lim_inf Y by A7,YELLOW_0:def 2; then p is_S-limit_of Y9 by A3; hence thesis by A2,A3,Def8; end; end; theorem Th35: :: YELLOW_6:32 for S being non empty 1-sorted, N being net of S, X being set for M being subnet of N st M = N"X for i being Element of M holds M.i in X proof let S be non empty 1-sorted, N be net of S, X be set; let M be subnet of N such that A1: M = N"X; let j be Element of M; j in the carrier of M; then j in (the mapping of N)"X by A1,YELLOW_6:def 10; then A2: (the mapping of N).j in X by FUNCT_1:def 7; the mapping of M = (the mapping of N)|the carrier of M by A1,YELLOW_6:def 6; hence thesis by A2,FUNCT_1:49; end; definition let L be non empty reflexive RelStr; func sigma L -> Subset-Family of L equals the topology of ConvergenceSpace Scott-Convergence L; coherence by YELLOW_6:def 24; end; theorem Th36: :: 1.5 Examples (5), p.100 for L being continuous complete Scott TopLattice, x be Element of L holds wayabove x is open proof let L be continuous complete Scott TopLattice, x be Element of L; set W = wayabove x; W is inaccessible proof let D be non empty directed Subset of L; assume sup D in W; then x << sup D by WAYBEL_3:8; then consider d being Element of L such that A1: d in D and A2: x << d by WAYBEL_4:53; d in W by A2; hence thesis by A1,XBOOLE_0:3; end; hence thesis by Def4; end; theorem Th37: for T being complete TopLattice st the topology of T = sigma T holds T is Scott proof let T be complete TopLattice; set CSC = ConvergenceSpace Scott-Convergence T; assume the topology of T = sigma T; then the TopStruct of T = TopStruct(#the carrier of CSC, the topology of CSC#) by YELLOW_6:def 24; hence thesis by Th34; end; :: non automated structural loci : Lm3: for T1,T2 being TopStruct st the TopStruct of T1 = the TopStruct of T2 & T1 is TopSpace-like holds T2 is TopSpace-like; Lm4: for S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 for N being strict net of S1 holds N is strict net of S2; Lm5: for S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds NetUniv S1 = NetUniv S2 proof let S1,S2 be non empty 1-sorted; assume A1: the carrier of S1 = the carrier of S2; defpred P[set] means ex N being strict net of S2 st N = $1 & the carrier of N in the_universe_of the carrier of S2; A2: now let x be set; hereby assume x in NetUniv S1; then consider N being strict net of S1 such that A3: N = x and A4: the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def 11; reconsider N as strict net of S2 by A1; thus P[x] proof take N; thus thesis by A1,A3,A4; end; end; assume P[x]; then consider N being strict net of S2 such that A5: N = x and A6: the carrier of N in the_universe_of the carrier of S2; reconsider N as strict net of S1 by A1; now take N; thus N = x & the carrier of N in the_universe_of the carrier of S1 by A1,A5,A6; end; hence x in NetUniv S1 by YELLOW_6:def 11; end; A7: for x being set holds x in NetUniv S2 iff P[x] by YELLOW_6:def 11; thus NetUniv S1 = NetUniv S2 from XFAMILY:sch 2(A2,A7); end; Lm6: for T1,T2 being non empty 1-sorted, X be set for N1 being net of T1, N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds N2 is_eventually_in X proof let T1,T2 be non empty 1-sorted, X be set; let N1 be net of T1, N2 be net of T2 such that A1: N1 = N2; assume N1 is_eventually_in X; then consider i being Element of N1 such that A2: for j being Element of N1 st i <= j holds N1.j in X; reconsider ii = i as Element of N2 by A1; take ii; let jj be Element of N2; reconsider j = jj as Element of N1 by A1; assume A3: ii <= jj; N2.jj = N1.j by A1; hence thesis by A1,A2,A3; end; Lm7: for T1,T2 being non empty TopSpace st the TopStruct of T1 = the TopStruct of T2 for N1 being net of T1, N2 being net of T2 st N1 = N2 for p1 being Point of T1, p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 proof let T1,T2 be non empty TopSpace such that A1: the TopStruct of T1 = the TopStruct of T2; let N1 be net of T1, N2 be net of T2 such that A2: N1 = N2; let p1 be Point of T1, p2 be Point of T2 such that A3: p1 = p2 and A4: p1 in Lim N1; for V being a_neighborhood of p2 holds N2 is_eventually_in V proof let V be a_neighborhood of p2; reconsider W = V as Subset of T1 by A1; p2 in Int V by CONNSP_2:def 1; then consider G being Subset of T2 such that A5: G is open and A6: G c= V and A7: p2 in G by TOPS_1:22; reconsider H = G as Subset of T1 by A1; G in the topology of T2 by A5; then H is open by A1; then p1 in Int W by A3,A6,A7,TOPS_1:22; then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def 1; thus N2 is_eventually_in V proof N1 is_eventually_in W by A4,YELLOW_6:def 15; then consider i being Element of N1 such that A8: for j being Element of N1 st i <= j holds N1.j in W; reconsider ii = i as Element of N2 by A2; take ii; let jj be Element of N2; reconsider j = jj as Element of N1 by A2; assume A9: ii <= jj; N2.jj = N1.j by A2; hence thesis by A2,A8,A9; end; end; hence thesis by YELLOW_6:def 15; end; Lm8: for T1,T2 being non empty TopSpace st the TopStruct of T1 = the TopStruct of T2 holds Convergence T1 = Convergence T2 proof let T1,T2 be non empty TopSpace such that A1: the TopStruct of T1 = the TopStruct of T2; A2: Convergence T1 c= [:NetUniv T1,the carrier of T1:] by YELLOW_6:def 18; A3: Convergence T2 c= [:NetUniv T2,the carrier of T2:] by YELLOW_6:def 18; let u1,u2 be object; hereby assume A4: [u1,u2] in Convergence T1; then consider N1 being Element of NetUniv T1, p1 being Point of T1 such that A5: [u1,u2] = [N1,p1] by A2,DOMAIN_1:1; A6: N1 in NetUniv T1; ex N being strict net of T1 st N = N1 & the carrier of N in the_universe_of the carrier of T1 by YELLOW_6:def 11; then reconsider N1 as net of T1; A7: p1 in Lim N1 by A4,A5,YELLOW_6:def 19; reconsider N2 = N1 as net of T2 by A1; reconsider p2 =p1 as Point of T2 by A1; A8: N2 in NetUniv T2 by A1,A6,Lm5; p2 in Lim N2 by A1,A7,Lm7; hence [u1,u2] in Convergence T2 by A5,A8,YELLOW_6:def 19; end; assume A9: [u1,u2] in Convergence T2; then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that A10: [u1,u2] = [N1,p1] by A3,DOMAIN_1:1; A11: N1 in NetUniv T2; ex N being strict net of T2 st N = N1 & the carrier of N in the_universe_of the carrier of T2 by YELLOW_6:def 11; then reconsider N1 as net of T2; A12: p1 in Lim N1 by A9,A10,YELLOW_6:def 19; reconsider N2 = N1 as net of T1 by A1; reconsider p2 =p1 as Point of T1 by A1; A13: N2 in NetUniv T1 by A1,A11,Lm5; p2 in Lim N2 by A1,A12,Lm7; hence thesis by A10,A13,YELLOW_6:def 19; end; Lm9: for R1,R2 being non empty RelStr st the RelStr of R1 = the RelStr of R2 & R1 is LATTICE holds R2 is LATTICE proof let R1,R2 be non empty RelStr such that A1: the RelStr of R1 = the RelStr of R2 and A2: R1 is LATTICE; A3: R2 is with_infima proof let x,y be Element of R2; reconsider x9 = x, y9 = y as Element of R1 by A1; consider z9 being Element of R1 such that A4: z9 <= x9 and A5: z9 <= y9 and A6: for w9 being Element of R1 st w9 <= x9 & w9 <= y9 holds w9 <= z9 by A2,LATTICE3:def 11; reconsider z = z9 as Element of R2 by A1; take z; thus z <= x & z <= y by A1,A4,A5,Lm1; let w be Element of R2; reconsider w9 = w as Element of R1 by A1; assume that A7: w <= x and A8: w <= y; A9: w9 <= x9 by A1,A7,Lm1; w9 <= y9 by A1,A8,Lm1; then w9 <= z9 by A6,A9; hence thesis by A1,Lm1; end; A10: R2 is with_suprema proof let x,y be Element of R2; reconsider x9 = x, y9 = y as Element of R1 by A1; consider z9 being Element of R1 such that A11: z9 >= x9 and A12: z9 >= y9 and A13: for w9 being Element of R1 st w9 >= x9 & w9 >= y9 holds w9 >= z9 by A2,LATTICE3:def 10; reconsider z = z9 as Element of R2 by A1; take z; thus z >= x & z >= y by A1,A11,A12,Lm1; let w be Element of R2; reconsider w9 = w as Element of R1 by A1; assume that A14: w >= x and A15: w >= y; A16: w9 >= x9 by A1,A14,Lm1; w9 >= y9 by A1,A15,Lm1; then w9 >= z9 by A13,A16; hence thesis by A1,Lm1; end; A17: R2 is reflexive by A1,A2,YELLOW_0:def 1,Lm1; A18: R2 is transitive proof let x,y,z be Element of R2; reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1; assume that A19: x <= y and A20: y <= z; A21: x9 <= y9 by A1,A19,Lm1; y9 <= z9 by A1,A20,Lm1; then x9 <= z9 by A2,A21,YELLOW_0:def 2; hence thesis by A1,Lm1; end; R2 is antisymmetric proof let x,y be Element of R2; reconsider x9 = x, y9 = y as Element of R1 by A1; assume that A22: x <= y and A23: y <= x; A24: x9 <= y9 by A1,A22,Lm1; y9 <= x9 by A1,A23,Lm1; hence thesis by A2,A24,YELLOW_0:def 3; end; hence thesis by A3,A10,A17,A18; end; Lm10: for R1,R2 being LATTICE, X being set st the RelStr of R1 = the RelStr of R2 for p1 being Element of R1, p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 by Lm1; Lm11: for R1,R2 being LATTICE, X being set st the RelStr of R1 = the RelStr of R2 for p1 being Element of R1, p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 by Lm1; Lm12: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 for D being set holds "\/"(D,R1) = "\/"(D,R2) proof let R1,R2 be complete LATTICE such that A1: the RelStr of R1 = the RelStr of R2; let D be set; reconsider b = "\/"(D,R1) as Element of R2 by A1; A2: ex_sup_of D,R2 by YELLOW_0:17; A3: ex_sup_of D,R1 by YELLOW_0:17; then D is_<=_than "\/"(D,R1) by YELLOW_0:def 9; then A4: D is_<=_than b by A1,Lm10; for a being Element of R2 st D is_<=_than a holds a >= b proof let a be Element of R2; reconsider a9 = a as Element of R1 by A1; assume D is_<=_than a; then D is_<=_than a9 by A1,Lm10; then a9 >= "\/"(D,R1) by A3,YELLOW_0:def 9; hence thesis by A1,Lm1; end; hence thesis by A2,A4,YELLOW_0:def 9; end; Lm13: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 for D being set holds "/\"(D,R1) = "/\"(D,R2) proof let R1,R2 be complete LATTICE such that A1: the RelStr of R1 = the RelStr of R2; let D be set; reconsider b = "/\"(D,R1) as Element of R2 by A1; A2: ex_inf_of D,R2 by YELLOW_0:17; A3: ex_inf_of D,R1 by YELLOW_0:17; then D is_>=_than "/\"(D,R1) by YELLOW_0:def 10; then A4: D is_>=_than b by A1,Lm11; for a being Element of R2 st D is_>=_than a holds a <= b proof let a be Element of R2; reconsider a9 = a as Element of R1 by A1; assume D is_>=_than a; then D is_>=_than a9 by A1,Lm11; then a9 <= "/\"(D,R1) by A3,YELLOW_0:def 10; hence thesis by A1,Lm1; end; hence thesis by A2,A4,YELLOW_0:def 10; end; Lm14: for R1,R2 being non empty reflexive RelStr st the RelStr of R1 = the RelStr of R2 for D being Subset of R1, D9 being Subset of R2 st D = D9 & D is directed holds D9 is directed proof let R1,R2 be non empty reflexive RelStr such that A1: the RelStr of R1 = the RelStr of R2; let D be Subset of R1, D9 be Subset of R2 such that A2: D = D9 and A3: D is directed; let x2,y2 be Element of R2 such that A4: x2 in D9 and A5: y2 in D9; reconsider x1 = x2, y1 = y2 as Element of R1 by A1; consider z1 being Element of R1 such that A6: z1 in D and A7: x1 <= z1 and A8: y1 <= z1 by A2,A3,A4,A5; reconsider z2 = z1 as Element of R2 by A1; take z2; thus z2 in D9 by A2,A6; thus x2 <= z2 & y2 <= z2 by A1,A7,A8,Lm1; end; Lm15: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 for p,q being Element of R1 st p << q for p9,q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9 proof let R1,R2 be complete LATTICE such that A1: the RelStr of R1 = the RelStr of R2; let p,q be Element of R1 such that A2: p << q; let p9,q9 be Element of R2 such that A3: p = p9 and A4: q = q9; let D9 be non empty directed Subset of R2 such that A5: q9 <= sup D9; reconsider D = D9 as non empty Subset of R1 by A1; reconsider D as non empty directed Subset of R1 by A1,Lm14; sup D = sup D9 by A1,Lm12; then q <= sup D by A1,A4,A5,Lm1; then consider d be Element of R1 such that A6: d in D and A7: p <= d by A2; reconsider d9 = d as Element of R2 by A1; take d9; thus d9 in D9 by A6; thus thesis by A1,A3,A7,Lm1; end; Lm16: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 for N1 being net of R1, N2 being net of R2 st N1 = N2 holds lim_inf N1 = lim_inf N2 proof let R1,R2 be complete LATTICE such that A1: the RelStr of R1 = the RelStr of R2; let N1 be net of R1, N2 be net of R2 such that A2: N1 = N2; set X1 = the set of all "/\"({N1.i where i is Element of N1: i >= j},R1) where j is Element of N1; set X2 = the set of all "/\"({N2.i where i is Element of N2: i >= j},R2) where j is Element of N2; X1 = X2 proof thus X1 c= X2 proof let e be object; assume e in X1; then consider j1 being Element of N1 such that A3: e = "/\"({N1.i where i is Element of N1: i >= j1},R1); reconsider j2 = j1 as Element of N2 by A2; set Y1 = {N1.i where i is Element of N1: i >= j1}, Y2 = {N2.i where i is Element of N2: i >= j2}; Y1 = Y2 proof thus Y1 c= Y2 proof let u be object; assume u in Y1; then consider i1 being Element of N1 such that A4: u = N1.i1 and A5: j1 <= i1; reconsider i2 = i1 as Element of N2 by A2; N2.i2 = u by A2,A4; hence thesis by A2,A5; end; let u be object; assume u in Y2; then consider i2 being Element of N2 such that A6: u = N2.i2 and A7: j2 <= i2; reconsider i1 = i2 as Element of N1 by A2; N1.i1 = u by A2,A6; hence thesis by A2,A7; end; then e = "/\"(Y2,R2) by A1,A3,Lm13; hence thesis; end; let e be object; assume e in X2; then consider j1 being Element of N2 such that A8: e = "/\"({N2.i where i is Element of N2: i >= j1},R2); reconsider j2 = j1 as Element of N1 by A2; set Y1 = {N2.i where i is Element of N2: i >= j1}, Y2 = {N1.i where i is Element of N1: i >= j2}; Y1 = Y2 proof thus Y1 c= Y2 proof let u be object; assume u in Y1; then consider i1 being Element of N2 such that A9: u = N2.i1 and A10: j1 <= i1; reconsider i2 = i1 as Element of N1 by A2; N1.i2 = u by A2,A9; hence thesis by A2,A10; end; let u be object; assume u in Y2; then consider i2 being Element of N1 such that A11: u = N1.i2 and A12: j2 <= i2; reconsider i1 = i2 as Element of N2 by A2; N2.i1 = u by A2,A11; hence thesis by A2,A12; end; then e = "/\"(Y2,R1) by A1,A8,Lm13; hence thesis; end; hence thesis by A1,Lm12; end; Lm17: for R1,R2 being non empty reflexive RelStr, X being non empty set for N1 being net of R1, N2 being net of R2 st N1 = N2 for J1 being net_set of the carrier of N1,R1, J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 proof let R1,R2 be non empty reflexive RelStr, X be non empty set; let N1 be net of R1, N2 be net of R2 such that A1: N1 = N2; let J1 be net_set of the carrier of N1,R1, J2 be net_set of the carrier of N2,R2 such that A2: J1 = J2; A3: the RelStr of Iterated J1 = [:N1, product J1:] by YELLOW_6:def 13; A4: the RelStr of Iterated J2 = [:N2, product J2:] by YELLOW_6:def 13; set f = the mapping of Iterated J1, g = the mapping of Iterated J2; A5: dom f = the carrier of Iterated J2 by A1,A2,A3,A4,FUNCT_2:def 1 .= dom g by FUNCT_2:def 1; for x being object st x in dom f holds f.x = g.x proof let x be object; assume x in dom f; then x in the carrier of Iterated J1; then x in [:the carrier of N1, the carrier of product J1:] by A3,YELLOW_3:def 2; then consider x1 being Element of N1, x2 being Element of product J1 such that A6: x = [x1,x2] by DOMAIN_1:1; reconsider y1 = x1 as Element of N2 by A1; reconsider y2 = x2 as Element of product J2 by A1,A2; thus f.x = (the mapping of Iterated J1).(x1,x2) by A6 .= (the mapping of J1.x1).(x2.x1) by YELLOW_6:def 13 .= (the mapping of J2.y1).(y2.y1) by A2 .= (the mapping of Iterated J2).(y1,y2) by YELLOW_6:def 13 .= g.x by A6; end; then f = g by A5,FUNCT_1:2; hence thesis by A1,A2,A3,A4; end; Lm18: for R1,R2 being non empty reflexive RelStr, X being non empty set st the RelStr of R1 = the RelStr of R2 for N1 being net of R1, N2 being net of R2 st N1 = N2 for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 proof let R1,R2 be non empty reflexive RelStr, X be non empty set such that A1: the RelStr of R1 = the RelStr of R2; let N1 be net of R1, N2 be net of R2 such that A2: N1 = N2; let J1 be net_set of the carrier of N1,R1; reconsider J2 = J1 as ManySortedSet of the carrier of N2 by A2; for i being set st i in rng J2 holds i is net of R2 proof let i be set; assume i in rng J2; then reconsider N = i as net of R1 by YELLOW_6:def 12; N is NetStr over R2 by A1; hence thesis; end; hence thesis by YELLOW_6:def 12; end; Lm19: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 holds Scott-Convergence R1 c= Scott-Convergence R2 proof let R1,R2 be complete LATTICE such that A1: the RelStr of R1 = the RelStr of R2; A2: Scott-Convergence R1 c= [:NetUniv R1,the carrier of R1:] by YELLOW_6:def 18; for e being object st e in Scott-Convergence R1 holds e in Scott-Convergence R2 proof let e be object; assume A3: e in Scott-Convergence R1; then consider N1 being Element of NetUniv R1, p1 being Element of R1 such that A4: e = [N1,p1] by A2,DOMAIN_1:1; A5: N1 in NetUniv R1; A6: ex N being strict net of R1 st ( N1 = N)&( the carrier of N in the_universe_of the carrier of R1) by YELLOW_6:def 11; then reconsider N2 = N1 as strict net of R2 by A1,Lm4; reconsider N1 as strict net of R1 by A6; reconsider p2 = p1 as Element of R2 by A1; A7: N2 in NetUniv R2 by A1,A5,Lm5; A8: lim_inf N1 = lim_inf N2 by A1,Lm16; p1 is_S-limit_of N1 by A3,A4,Def8; then p1 <= lim_inf N1; then p2 <= lim_inf N2 by A1,A8,Lm1; then p2 is_S-limit_of N2; hence thesis by A4,A7,Def8; end; hence thesis; end; Lm20: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 holds Scott-Convergence R1 = Scott-Convergence R2 by Lm19; Lm21: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 holds sigma R1 = sigma R2 proof let R1,R2 be complete LATTICE; assume A1: the RelStr of R1 = the RelStr of R2; set T1 = ConvergenceSpace Scott-Convergence R1, T2 = ConvergenceSpace Scott-Convergence R2; A2: the topology of T1 = { V where V is Subset of R1: for p being Element of R1 st p in V for N being net of R1 st [N,p] in Scott-Convergence R1 holds N is_eventually_in V} by YELLOW_6:def 24; A3: the topology of T2 = { V where V is Subset of R2: for p being Element of R2 st p in V for N being net of R2 st [N,p] in Scott-Convergence R2 holds N is_eventually_in V} by YELLOW_6:def 24; the topology of T1 = the topology of T2 proof thus the topology of T1 c= the topology of T2 proof let e be object; assume e in the topology of T1; then consider V1 being Subset of R1 such that A4: e = V1 and A5: for p being Element of R1 st p in V1 for N being net of R1 st [N,p] in Scott-Convergence R1 holds N is_eventually_in V1 by A2; reconsider V2 = V1 as Subset of R2 by A1; for p being Element of R2 st p in V2 for N being net of R2 st [N,p] in Scott-Convergence R2 holds N is_eventually_in V2 proof let p2 be Element of R2 such that A6: p2 in V2; reconsider p1 = p2 as Element of R1 by A1; let N2 be net of R2; reconsider N1 = N2 as net of R1 by A1; assume [N2,p2] in Scott-Convergence R2; then [N1,p1] in Scott-Convergence R1 by A1,Lm20; hence thesis by A5,A6,Lm6; end; hence thesis by A3,A4; end; let e be object; assume e in the topology of T2; then consider V1 being Subset of R2 such that A7: e = V1 and A8: for p being Element of R2 st p in V1 for N being net of R2 st [N,p] in Scott-Convergence R2 holds N is_eventually_in V1 by A3; reconsider V2 = V1 as Subset of R1 by A1; for p being Element of R1 st p in V2 for N being net of R1 st [N,p] in Scott-Convergence R1 holds N is_eventually_in V2 proof let p2 be Element of R1 such that A9: p2 in V2; reconsider p1 = p2 as Element of R2 by A1; let N2 be net of R1; reconsider N1 = N2 as net of R2 by A1; assume [N2,p2] in Scott-Convergence R1; then [N1,p1] in Scott-Convergence R2 by A1,Lm20; hence thesis by A8,A9,Lm6; end; hence thesis by A2,A7; end; hence thesis; end; Lm22: for R1,R2 being LATTICE st the RelStr of R1 = the RelStr of R2 & R1 is complete holds R2 is complete proof let R1,R2 be LATTICE such that A1: the RelStr of R1 = the RelStr of R2 and A2: R1 is complete; let X be set; consider a1 being Element of R1 such that A3: X is_<=_than a1 and A4: for b being Element of R1 st X is_<=_than b holds a1 <= b by A2; reconsider a2 = a1 as Element of R2 by A1; take a2; thus X is_<=_than a2 by A1,A3,Lm10; let b2 be Element of R2; reconsider b1 = b2 as Element of R1 by A1; assume X is_<=_than b2; then X is_<=_than b1 by A1,Lm10; hence a2 <= b2 by A1,A4,Lm1; end; Lm23: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 & R1 is continuous holds R2 is continuous proof let R1,R2 be complete LATTICE such that A1: the RelStr of R1 = the RelStr of R2; assume A2: R1 is continuous; thus A3: for x being Element of R2 holds waybelow x is non empty directed; thus R2 is up-complete; for x,y being Element of R2 st not x <= y ex u being Element of R2 st u << x & not u <= y proof let x2,y2 be Element of R2; reconsider x1=x2, y1=y2 as Element of R1 by A1; assume not x2 <= y2; then not x1 <= y1 by A1,Lm1; then consider u1 be Element of R1 such that A4: u1 << x1 and A5: not u1 <= y1 by A2,WAYBEL_3:24; reconsider u2 = u1 as Element of R2 by A1; take u2; thus u2 << x2 by A1,A4,Lm15; thus thesis by A1,A5,Lm1; end; hence thesis by A3,WAYBEL_3:24; end; registration let R be continuous complete LATTICE; :: 1.6. Proposition (ii) cluster Scott-Convergence R -> topological; coherence proof set C = Scott-Convergence R; thus C is (CONSTANTS) (SUBNETS); thus C is (DIVERGENCE) proof let X be net of R, p be Element of R such that A1: X in NetUniv R and A2: not [X,p] in C; A3: for x being Element of R holds waybelow x is non empty directed; reconsider p9 = p as Element of R; consider N being strict net of R such that A4: N = X and the carrier of N in the_universe_of the carrier of R by A1,YELLOW_6:def 11; not p is_S-limit_of N by A1,A2,A4,Def8; then not p <= lim_inf X by A4; then consider u being Element of R such that A5: u << p9 and A6: not u <= lim_inf X by A3,WAYBEL_3:24; set A = { a where a is Element of R : not a >= u}; X is_often_in A proof let i be Element of X; set B = { X.j where j is Element of X: j >= i}; set C = the set of all "/\"({X.k where k is Element of X: k >= j},R) where j is Element of X; "/\"(B,R) in C; then "/\"(B,R) <= lim_inf X by YELLOW_2:22; then not u <= "/\"(B,R) by A6,YELLOW_0:def 2; then not u is_<=_than B by YELLOW_0:33; then consider b being Element of R such that A7: b in B and A8: not u <= b; consider j being Element of X such that A9: b = X.j and A10: j >= i by A7; take j; thus i <= j by A10; thus thesis by A8,A9; end; then reconsider Y = X"A as subnet of X by YELLOW_6:22; take Y; reconsider UN = the_universe_of the carrier of R as universal set; A11: ex N being strict net of R st X = N & the carrier of N in UN by A1,YELLOW_6:def 11; X"A is SubRelStr of X by YELLOW_6:def 6; then the carrier of X"A c= the carrier of X by YELLOW_0:def 13; then the carrier of Y in UN by A11,CLASSES1:def 1; hence Y in NetUniv R by YELLOW_6:def 11; let Z be subnet of Y; assume A12: [Z,p] in C; C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18; then A13: Z in NetUniv R by A12,ZFMISC_1:87; then consider ZZ being strict net of R such that A14: ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def 11; deffunc F(Element of Z) = "/\"({Z.i where i is Element of Z: i >= $1},R); set D = {F(j) where j is Element of Z: P[j]}; D is Subset of R from DOMAIN_1:sch 8; then reconsider D as Subset of R; reconsider D as non empty directed Subset of R by Th30; p is_S-limit_of ZZ by A12,A13,A14,Def8; then p <= lim_inf Z by A14; then consider d being Element of R such that A15: d in D and A16: u <= d by A5; consider j being Element of Z such that A17: d = "/\"({Z.k where k is Element of Z: k >= j},R) by A15; reconsider j9 = j as Element of Z; consider i being Element of Z such that A18: i >= j9 and i >= j9 by YELLOW_6:def 3; consider f being Function of Z, Y such that A19: the mapping of Z = (the mapping of Y)*f and for m being Element of Y ex n being Element of Z st for p being Element of Z st n <= p holds m <= f.p by YELLOW_6:def 9; Z.i in {Z.k where k is Element of Z: k >= j} by A18; then A20: d <= Z.i by A17,YELLOW_2:22; Y.(f.i) = Z.i by A19,FUNCT_2:15; then Z.i in A by Th35; then ex a being Element of R st a = Z.i & not a >= u; hence contradiction by A16,A20,YELLOW_0:def 2; end; thus C is (ITERATED_LIMITS) proof let X be net of R, p be Element of R such that A21: [X,p] in C; let J be net_set of the carrier of X, R such that A22: for i being Element of X holds [J.i,X.i] in C; A23: C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18; then A24: X in NetUniv R by A21,ZFMISC_1:87; for i being Element of X holds J.i in NetUniv R proof let i be Element of X; [J.i,X.i] in C by A22; hence thesis by A23,ZFMISC_1:87; end; then A25: Iterated J in NetUniv R by A24,YELLOW_6:25; reconsider p9 = p as Element of R; set q = lim_inf Iterated J; q is_>=_than waybelow p9 proof let u be Element of R; assume u in waybelow p9; then A26: u << p9 by WAYBEL_3:7; set T = TopRelStr(#the carrier of R,the InternalRel of R, sigma R#); A27: the RelStr of T = the RelStr of R; A28: the carrier of R = the carrier of ConvergenceSpace C by YELLOW_6:def 24; then reconsider T as TopLattice by A27,Lm3,Lm9; reconsider T as complete TopLattice by A27,Lm22; reconsider T as continuous complete TopLattice by A27,Lm23; the topology of T = sigma T by A27,Lm21; then reconsider T as continuous complete Scott TopLattice by Th37; :: we now move all to T setting reconsider XX = X as net of T; reconsider JJ = J as net_set of the carrier of XX,T by A27,Lm18; reconsider uu = u, qq = q, pp = p9 as Element of T; set N = Iterated JJ; set CC = Convergence T; CC = Convergence ConvergenceSpace C by A28,Lm8; then A29: C c= CC by YELLOW_6:40; A30: uu << pp by A26,A27,Lm15; A31: qq = lim_inf N by A27,Lm16,Lm17; for i being Element of XX holds [JJ.i,XX.i] in CC proof let i be Element of XX; reconsider ii = i as Element of X; [J.ii,X.ii] in C by A22; hence thesis by A29; end; then [N,pp] in CC by A21,A29,YELLOW_6:def 23; then A32: pp in Lim N by YELLOW_6:def 19; pp in wayabove uu by A30; then wayabove uu is a_neighborhood of pp by Th36,CONNSP_2:3; then A33: N is_eventually_in wayabove uu by A32,YELLOW_6:def 15; wayabove uu c= uparrow uu by WAYBEL_3:11; then N is_eventually_in uparrow uu by A33,WAYBEL_0:8; hence u <= q by A27,A31,Lm1,Th18; end; then sup waybelow p9 <= q by YELLOW_0:32; then p <= q by WAYBEL_3:def 5; then p is_S-limit_of Iterated J; hence thesis by A25,Def8; end; end; end; theorem :: Corrollary to Proposition 1.6 (p.103) for T be continuous complete Scott TopLattice, x be Element of T, N be net of T st N in NetUniv T holds x is_S-limit_of N iff x in Lim N proof let T be continuous complete Scott TopLattice, x be Element of T, N be net of T such that A1: N in NetUniv T; A2: Convergence ConvergenceSpace Scott-Convergence T = Scott-Convergence T by YELLOW_6:44; consider M being strict net of T such that A3: M = N and the carrier of M in the_universe_of the carrier of T by A1,YELLOW_6:def 11; the TopStruct of T = ConvergenceSpace Scott-Convergence T by Th32; then A4: Convergence T = Convergence ConvergenceSpace Scott-Convergence T by Lm8; thus x is_S-limit_of N implies x in Lim N proof assume x is_S-limit_of N; then [N,x] in Convergence T by A1,A2,A3,A4,Def8; hence thesis by YELLOW_6:def 19; end; assume x in Lim N; then [M,x] in Scott-Convergence T by A1,A2,A3,A4,YELLOW_6:def 19; hence thesis by A1,A3,Def8; end; theorem Th39: :: 1.7. Lemma for L being complete non empty Poset st Scott-Convergence L is (ITERATED_LIMITS) holds L is continuous proof let L be complete non empty Poset such that A1: Scott-Convergence L is (ITERATED_LIMITS); set C = Scott-Convergence L; now let I be non empty set such that A2: I in the_universe_of the carrier of L; let K be non-empty ManySortedSet of I such that A3: for j being Element of I holds K.j in the_universe_of the carrier of L; let F be DoubleIndexedSet of K, L such that A4: for j being Element of I holds rng(F.j) is directed; set x = Inf Sups F; A5: x >= Sup Infs Frege F by WAYBEL_5:16; [:I,I:] c= [:I,I:]; then reconsider r = [:I,I:] as Relation of I; dom F = I by PARTFUN1:def 2; then reconsider f = Sups F as Function of I, the carrier of L; set X = NetStr(#I,r,f#); A6: for i,j being Element of X holds i <= j proof let i,j be Element of X; [i,j] in the InternalRel of X by ZFMISC_1:87; hence thesis by ORDERS_2:def 5; end; A7: X is transitive by A6; X is directed proof let x,y be Element of X; take x; thus thesis by A6; end; then reconsider X = NetStr(#I,r,f#) as strict net of L by A7; deffunc F(Element of I) = Net-Str(K.$1,F.$1); consider J being ManySortedSet of I such that A8: for i being Element of I holds J.i = F(i) from PBOOLE:sch 5; for i being set st i in the carrier of X holds J.i is net of L proof let i be set; assume i in the carrier of X; then reconsider i9 = i as Element of I; reconsider rFi = rng(F.i9) as Subset of L; A9: rFi is directed by A4; J.i9 = Net-Str(K.i9,F.i9) by A8; hence thesis by A9,Th20; end; then reconsider J as net_set of the carrier of X, L by YELLOW_6:24; A10: for j be set st j in I ex R being 1-sorted st R = J.j & K.j = the carrier of R proof let i be set; assume i in I; then reconsider i9 = i as Element of I; take R = Net-Str(K.i9,F.i9); thus R = J.i by A8; thus thesis by Def10; end; A11: doms F = K by YELLOW_7:45 .= Carrier J by A10,PRALG_1:def 13; A12: dom Frege F = product doms F by PARTFUN1:def 2; then A13: dom Infs Frege F = product doms F by FUNCT_2:def 1; A14: for i being Element of X holds J.i in NetUniv L proof let i be Element of X; reconsider i9 = i as Element of I; A15: J.i = Net-Str(K.i9,F.i9) by A8; then reconsider Ji = J.i as strict net of L; K.i9 in the_universe_of the carrier of L by A3; then the carrier of Ji in the_universe_of the carrier of L by A15,Def10; hence thesis by YELLOW_6:def 11; end; A16: for i being Element of X holds [J.i,X.i] in C proof let i be Element of X; reconsider i9 = i as Element of I; A17: J.i = Net-Str(K.i9,F.i9) by A8; then reconsider Ji = J.i as monotone reflexive net of L; A18: J.i in NetUniv L by A14; i in I; then i9 in dom F by PARTFUN1:def 2; then X.i = Sup(F.i9) by WAYBEL_5:def 1 .= Sup the mapping of Ji by A17,Def10 .= sup Ji by WAYBEL_2:def 1 .= lim_inf Ji by Th22; then X.i is_S-limit_of J.i; hence thesis by A17,A18,Def8; end; A19: X in NetUniv L by A2,YELLOW_6:def 11; then A20: Iterated J in NetUniv L by A14,YELLOW_6:25; deffunc I(Element of Iterated J) = {(Iterated J).p where p is Element of Iterated J :p >= $1}; the carrier of Iterated J = [:the carrier of X, product Carrier J:] by YELLOW_6:26; then reconsider G = the mapping of Iterated J as Function of [:the carrier of X, product doms F:], the carrier of L by A11; deffunc I(Element of X, Element of product doms F) = {G.(i,$2) where i is Element of X :i >= $1}; deffunc F(Element of product doms F) = "/\"(rng((Frege F).$1),L); deffunc F(Element of X, Element of product doms F) = "/\"(I($1,$2),L); set D = the set of all "/\"(I(j),L) where j is Element of Iterated J; set D9 = {F(i,g) where i is Element of X, g is Element of product doms F: P[g]}; set E9 = {F(g) where g is Element of product doms F : P[g]}; A21: for i being Element of X, g being Element of product doms F holds F(g) = F(i,g) proof let j be Element of X, g be Element of product doms F; for y being object holds y in I(j,g) iff ex x being object st x in dom((Frege F).g) & y = ((Frege F).g).x proof let y be object; g in product Carrier J by A11; then A22: g in the carrier of product J by YELLOW_1:def 4; hereby assume y in I(j,g); then consider i being Element of X such that A23: y =G.(i,g) and i >= j; reconsider x = i as object; take x; reconsider i9 = i as Element of I; A24: i in I; then A25: i9 in dom F by PARTFUN1:def 2; thus x in dom((Frege F).g) by A24,PARTFUN1:def 2; thus ((Frege F).g).x = F.i9.(g.i) by A12,A25,WAYBEL_5:9 .= (the mapping of Net-Str(K.i9,F.i9)).(g.i) by Def10 .= (the mapping of J.i).(g.i) by A8 .= y by A22,A23,YELLOW_6:def 13; end; given x being object such that A26: x in dom((Frege F).g) and A27: y = ((Frege F).g).x; A28: x in dom F by A12,A26,WAYBEL_5:8; reconsider i9 = x as Element of I by A26; reconsider i = i9 as Element of X; A29: i >= j by A6; y = (F.x).(g.x) by A12,A27,A28,WAYBEL_5:9 .= (the mapping of Net-Str(K.i9,F.i9)).(g.i) by Def10 .= (the mapping of J.i).(g.i) by A8 .= G.(i,g) by A22,YELLOW_6:def 13; hence thesis by A29; end; hence thesis by FUNCT_1:def 3; end; A30: D = D9 proof A31: the carrier of Iterated J = [:the carrier of X, product Carrier J:] by YELLOW_6:26; A32: for p being Element of Iterated J, i being Element of X, g being Element of product doms F st p = [i,g] holds "/\"(I(p),L) = "/\"(I(i,g),L) proof let p be Element of Iterated J, i be Element of X, g be Element of product doms F such that A33: p = [i,g]; A34: the RelStr of Iterated J= the RelStr of [:X, product J:] by YELLOW_6:def 13; reconsider g9 = g as Element of product J by A11,YELLOW_1:def 4; g9 in the carrier of product J; then A35: g9 in product Carrier J by YELLOW_1:def 4; reconsider i9 = i as Element of X; for i be object st i in the carrier of X ex R being RelStr, xi,yi being Element of R st R = J.i & xi = g9.i & yi = g9.i & xi <= yi proof let i be object; assume i in the carrier of X; then reconsider ii = i as Element of X; reconsider i9 = ii as Element of I; A36: J.i = Net-Str(K.i9,F.i9) by A8; set R = Net-Str(K.i9,F.i9); g9.ii in the carrier of R by A36; then reconsider x = g9.i as Element of R; take R,x,x; x <= x; hence thesis by A8; end; then A37: g9 <= g9 by A35,YELLOW_1:def 4; I(i,g) c= I(p) proof let u be object; assume u in I(i,g); then consider j being Element of X such that A38: u = (the mapping of Iterated J).(j,g) and A39: j >= i; reconsider j9 = j as Element of X; reconsider q = [j,g] as Element of Iterated J by A11,YELLOW_6:26; [j9,g9] >= [i9,g9] by A37,A39,YELLOW_3:11; then A40: q >= p by A33,A34,Lm1; u = (Iterated J).q by A38; hence thesis by A40; end; then A41: "/\"(I(p),L) <= "/\"(I(i,g),L) by WAYBEL_7:1; defpred P[Element of X] means $1 >= i; deffunc F(Element of X) = G.($1,g); {F(k) where k is Element of X: P[k]} is Subset of L from DOMAIN_1:sch 8; then reconsider A = I(i,g) as Subset of L; defpred P[Element of Iterated J] means $1 >= p; deffunc F(Element of Iterated J) = (Iterated J).$1; {F(z) where z is Element of Iterated J: P[z]} is Subset of L from DOMAIN_1:sch 8; then reconsider B = I(p) as Subset of L; B is_coarser_than A proof let b be Element of L; assume b in B; then consider q being Element of Iterated J such that A42: b = (Iterated J).q and A43: p <= q; consider k being Element of X, f being Element of product Carrier J such that A44: q = [k,f] by A31,DOMAIN_1:1; reconsider k9 = k as Element of X; set a = (the mapping of Iterated J).(k,g); a = G.(k,g); then reconsider a as Element of L; take a; reconsider f9 = f as Element of product J by YELLOW_1:def 4; A45: [k9,f9] >= [i9,g9] by A33,A34,A43,A44,Lm1; then i <= k by YELLOW_3:11; hence a in A; reconsider k9 = k as Element of I; set N = Net-Str(K.k9,F.k9); A46: J.k = N by A8; reconsider g9k =g9.k, f9k = f9.k as Element of N by A8; A47: b = N.(f9k) by A42,A44,A46,YELLOW_6:27; reconsider kg = [k,g] as Element of Iterated J by A11,YELLOW_6:26; A48: a = (Iterated J).kg .= N.(g9k) by A46,YELLOW_6:27; g9 <= f9 by A45,YELLOW_3:11; then g9.k <= f9.k by WAYBEL_3:28; hence a <= b by A46,A47,A48,Def10; end; then "/\"(I(i,g),L) <= "/\"(I(p),L) by Th1; hence thesis by A41,YELLOW_0:def 3; end; thus D c= D9 proof let e be object; assume e in D; then consider p being Element of Iterated J such that A49: e = "/\"(I(p),L); consider j being Element of X, g being Element of product doms F such that A50: p = [j,g] by A11,A31,DOMAIN_1:1; e = "/\"(I(j,g),L) by A32,A49,A50; hence thesis; end; let e be object; assume e in D9; then consider i being Element of X, g being Element of product doms F such that A51: e = "/\"(I(i,g),L); reconsider j = [i,g] as Element of Iterated J by A11,YELLOW_6:26; e = "/\"(I(j),L) by A32,A51; hence thesis; end; A52: E9 = D9 from Irrel(A21); :: UWAGA!!! wrazliwy na strony rownosci for y being object holds y in E9 iff ex x being object st x in dom(Infs Frege F) & y = (Infs Frege F).x proof let y be object; thus y in E9 implies ex x being object st x in dom(Infs Frege F) & y = (Infs Frege F).x proof assume y in E9; then consider g being Element of product doms F such that A53: y = "/\"(rng((Frege F).g),L); take g; thus A54: g in dom(Infs Frege F) by A13; thus y = //\((Frege F).g, L) by A53,YELLOW_2:def 6 .= (Infs Frege F).g by A54,WAYBEL_5:def 2; end; given x being object such that A55: x in dom(Infs Frege F) and A56: y = (Infs Frege F).x; reconsider x as Element of product doms F by A55,PARTFUN1:def 2; y = //\((Frege F).x, L) by A55,A56,WAYBEL_5:def 2 .= "/\"(rng((Frege F).x),L) by YELLOW_2:def 6; hence thesis; end; then rng Infs Frege F = E9 by FUNCT_1:def 3; then A57: Sup Infs Frege F = lim_inf Iterated J by A30,A52,YELLOW_2:def 5; reconsider x9 = x as Element of L; set X1 = the set of all x where j9 is Element of X; set X2 = the set of all "/\"({X.i where i is Element of X:i >= j},L) where j is Element of X; A58: X2 = X1 proof A59: for j being Element of X holds x = "/\"({X.i where i is Element of X:i >= j},L) proof let j be Element of X; set X3 = {X.i where i is Element of X:i >= j}; for e being object holds e in X3 iff ex u being object st u in dom Sups F & e = (Sups F).u proof let e be object; hereby assume e in X3; then consider i being Element of X such that A60: e = X.i and i >= j; reconsider u = i as object; take u; u in I; hence u in dom Sups F by FUNCT_2:def 1; thus e = (Sups F).u by A60; end; given u being object such that A61: u in dom Sups F and A62: e = (Sups F).u; reconsider i = u as Element of X by A61,FUNCT_2:def 1; A63: i >= j by A6; e = X.i by A62; hence thesis by A63; end; then rng Sups F = X3 by FUNCT_1:def 3; hence thesis by YELLOW_2:def 6; end; thus X2 c= X1 proof let u be object; assume u in X2; then ex j being Element of X st ( u = "/\"({X.i where i is Element of X:i >= j},L)); then u = x by A59; hence thesis; end; let u be object; set j = the Element of X; assume u in X1; then ex j being Element of X st u = x; then u = "/\"({X.i where i is Element of X:i >= j},L) by A59; hence thesis; end; now let u be object; u in X1 iff ex j9 being Element of X st u = x; then u in X1 iff u = x; hence u in X1 iff u in {x} by TARSKI:def 1; end; then "\/"(X2,L) = sup {x9} by A58,TARSKI:2 .= x by YELLOW_0:39; then x <= lim_inf X; then x is_S-limit_of X; then [X,x] in C by A19,Def8; then [Iterated J,x] in C by A1,A16; then x is_S-limit_of Iterated J by A20,Def8; then x <= Sup Infs Frege F by A57; hence x = Sup Infs Frege F by A5,ORDERS_2:2; end; hence thesis by WAYBEL_5:18; end; theorem :: 1.8 Theorem, p.104 for T being complete Scott TopLattice holds T is continuous iff Convergence T = Scott-Convergence T proof let T be complete Scott TopLattice; hereby assume T is continuous; then reconsider L = T as continuous complete Scott TopLattice; the TopStruct of T = ConvergenceSpace Scott-Convergence T by Th32; hence Convergence T = Convergence ConvergenceSpace Scott-Convergence L by Lm8 .= Scott-Convergence T by YELLOW_6:44; end; thus thesis by Th39; end; theorem Th41: :: 1.9 Remark, p.104 for T being complete Scott TopLattice, S being upper Subset of T st S is Open holds S is open proof let T be complete Scott TopLattice, S be upper Subset of T such that A1: for x be Element of T st x in S ex y be Element of T st y in S & y << x; S is inaccessible proof let D be non empty directed Subset of T; assume sup D in S; then consider y being Element of T such that A2: y in S and A3: y << sup D by A1; consider d being Element of T such that A4: d in D and A5: y <= d by A3; d in S by A2,A5,WAYBEL_0:def 20; hence thesis by A4,XBOOLE_0:3; end; hence thesis by Def4; end; theorem Th42: for L being non empty RelStr, S being upper Subset of L, x being Element of L st x in S holds uparrow x c= S proof let L be non empty RelStr, S be upper Subset of L, x be Element of L; assume A1: x in S; let e be object; assume A2: e in uparrow x; then reconsider y = e as Element of L; x <= y by A2,WAYBEL_0:18; hence thesis by A1,WAYBEL_0:def 20; end; theorem Th43: for L being complete continuous Scott TopLattice, p be Element of L, S be Subset of L st S is open & p in S ex q being Element of L st q << p & q in S proof let L be complete continuous Scott TopLattice, p be Element of L; let S be Subset of L such that A1: S is open and A2: p in S; A3: S is inaccessible by A1,Def4; sup waybelow p = p by WAYBEL_3:def 5; then waybelow p meets S by A2,A3; then (waybelow p) /\ S <> {}; then consider u being Element of L such that A4: u in (waybelow p) /\ S by SUBSET_1:4; reconsider u as Element of L; take u; u in waybelow p by A4,XBOOLE_0:def 4; hence u << p by WAYBEL_3:7; thus thesis by A4,XBOOLE_0:def 4; end; theorem Th44: :: 1.10. Propostion (i), p.104 for L being complete continuous Scott TopLattice, p be Element of L holds { wayabove q where q is Element of L: q << p } is Basis of p proof let L be complete continuous Scott TopLattice, p be Element of L; set X = { wayabove q where q is Element of L: q << p }; X c= bool the carrier of L proof let e be object; assume e in X; then ex q being Element of L st e = wayabove q & q << p; hence thesis; end; then reconsider X as Subset-Family of L; X is Basis of p proof A1: X is open proof let e be Subset of L; assume e in X; then consider q being Element of L such that A2: e = wayabove q and q << p; wayabove q is open by Th36; hence thesis by A2; end; X is p-quasi_basis proof for Y being set st Y in X holds p in Y proof let e be set; assume e in X; then ex q being Element of L st e = wayabove q & q << p; hence thesis; end; hence p in Intersect X by SETFAM_1:43; let S be Subset of L such that A3: S is open and A4: p in S; consider u being Element of L such that A5: u << p and A6: u in S by A3,A4,Th43; take V = wayabove u; thus V in X by A5; A7: S is upper by A3,Def4; A8: wayabove u c= uparrow u by WAYBEL_3:11; uparrow u c= S by A6,A7,Th42; hence thesis by A8; end; hence thesis by A1; end; hence thesis; end; theorem Th45: for T being complete continuous Scott TopLattice holds the set of all wayabove x where x is Element of T is Basis of T proof let T be complete continuous Scott TopLattice; set B = the set of all wayabove x where x is Element of T; A1: B c= the topology of T proof let e be object; assume e in B; then consider x being Element of T such that A2: e = wayabove x; wayabove x is open by Th36; hence thesis by A2; end; then reconsider P = B as Subset-Family of T by XBOOLE_1:1; for x being Point of T ex B being Basis of x st B c= P proof let x be Point of T; reconsider p = x as Element of T; reconsider A = { wayabove q where q is Element of T: q << p } as Basis of x by Th44; take A; let u be object; assume u in A; then ex q being Element of T st u = wayabove q & q << p; hence thesis; end; hence thesis by A1,YELLOW_8:14; end; theorem :: 1.10. Propostion (ii), p.104 for T being complete continuous Scott TopLattice, S being upper Subset of T holds S is open iff S is Open proof let T be complete continuous Scott TopLattice, S be upper Subset of T; thus S is open implies S is Open proof assume A1: S is open; let x be Element of T; assume x in S; then ex y be Element of T st y << x & y in S by A1,Th43; hence thesis; end; thus thesis by Th41; end; theorem :: 1.10. Propostion (iii), p.104 for T being complete continuous Scott TopLattice, p being Element of T holds Int uparrow p = wayabove p proof let T be complete continuous Scott TopLattice, p be Element of T; thus Int uparrow p c= wayabove p proof let y be object; assume A1: y in Int uparrow p; then reconsider q = y as Element of T; reconsider S = Int uparrow p as Subset of T; consider u being Element of T such that A2: u << q and A3: u in S by A1,Th43; S c= uparrow p by TOPS_1:16; then p <= u by A3,WAYBEL_0:18; then p << q by A2,WAYBEL_3:2; hence thesis; end; wayabove p c= uparrow p by WAYBEL_3:11; hence thesis by Th36,TOPS_1:24; end; theorem :: 1.10. Propostion (iv), p.104 for T being complete continuous Scott TopLattice, S being Subset of T holds Int S = union{wayabove x where x is Element of T: wayabove x c= S} proof let T be complete continuous Scott TopLattice, S be Subset of T; set B = the set of all wayabove x where x is Element of T; set I = { G where G is Subset of T: G in B & G c= S }, P = {wayabove x where x is Element of T: wayabove x c= S}; A1: I = P proof thus I c= P proof let e be object; assume e in I; then consider G being Subset of T such that A2: e = G and A3: G in B and A4: G c= S; ex x being Element of T st G = wayabove x by A3; hence thesis by A2,A4; end; let e be object; assume e in P; then consider x being Element of T such that A5: e = wayabove x and A6: wayabove x c= S; wayabove x in B; hence thesis by A5,A6; end; B is Basis of T by Th45; hence thesis by A1,YELLOW_8:11; end;