### The Mizar article:

### Scott Topology

**by****Andrzej Trybulec**

- Received January 29, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: WAYBEL11
- [ MML identifier index ]

environ vocabulary ORDERS_1, BHSP_3, WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, QUANTAL1, BOOLE, RELAT_2, FINSET_1, ORDINAL2, YELLOW_0, REALSET1, RELAT_1, SUBSET_1, WAYBEL_9, PRE_TOPC, NATTRA_1, T_0TOPSP, CONNSP_2, TOPS_1, TARSKI, FUNCT_1, YELLOW_6, SEQM_3, CLASSES1, ZF_LANG, YELLOW_2, PROB_1, WAYBEL_3, CARD_3, PBOOLE, CLOSURE1, ZF_REFLE, WAYBEL_5, FUNCT_6, RLVECT_2, WAYBEL_6, CANTOR_1, WAYBEL11, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, STRUCT_0, REALSET1, GROUP_1, WAYBEL_6, PRE_TOPC, TOPS_1, CANTOR_1, CONNSP_2, T_0TOPSP, TDLAT_3, PBOOLE, CLASSES1, CLASSES2, CARD_3, PRALG_1, ORDERS_1, 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 T_0TOPSP, TOPS_1, TDLAT_3, GROUP_1, WAYBEL_3, WAYBEL_5, YELLOW_4, CLASSES1, ORDERS_3, CANTOR_1, WAYBEL_9, YELLOW_8, WAYBEL_1, WAYBEL_6, PRALG_2, CLASSES2, CONNSP_2, MEMBERED, PARTFUN1; clusters YELLOW_0, STRUCT_0, WAYBEL_0, TDLAT_3, FINSET_1, WAYBEL_3, YELLOW_6, PBOOLE, RELSET_1, WAYBEL_5, PRALG_1, PRVECT_1, YELLOW_1, WAYBEL_9, LATTICE3, MSUALG_1, CLASSES2, SUBSET_1, FRAENKEL, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1; requirements SUBSET, BOOLE; definitions STRUCT_0, XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, GROUP_1, YELLOW_0, RELAT_1, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3, YELLOW_8, WAYBEL_6; theorems TSP_1, WAYBEL_0, PRE_TOPC, YELLOW_0, TARSKI, SUBSET_1, TOPS_1, YELLOW_2, SETFAM_1, CONNSP_2, ZFMISC_1, RELSET_1, TDLAT_3, TEX_1, ORDERS_1, GROUP_1, LATTICE3, YELLOW_6, WAYBEL_5, DOMAIN_1, WAYBEL_7, YELLOW_1, YELLOW_3, PBOOLE, BINOP_1, WAYBEL_3, FUNCT_1, FUNCT_2, YELLOW_7, PRALG_1, WAYBEL_2, CLASSES1, YELLOW_4, WAYBEL_1, RELAT_1, WAYBEL_4, CANTOR_1, YELLOW_8, XBOOLE_0, XBOOLE_1; schemes DOMAIN_1, RELSET_1, COMPLSP1, FRAENKEL, PRALG_2, XBOOLE_0; begin :: Preliminaries Lm1: for R,S being RelStr, p,q being Element of R, p',q' being Element of S st p = p' & q = q' & the RelStr of R = the RelStr of S holds p <= q implies p' <= q' proof let R,S be RelStr, p,q be Element of R, p',q' be Element of S such that A1: p = p' & q = q' & the RelStr of R = the RelStr of S; assume p <= q; then [p',q'] in the InternalRel of S by A1,ORDERS_1:def 9; hence p' <= q' by ORDERS_1:def 9; 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 set; consider i being Element of I(); assume e in A; then consider u being Element of D() such that A2: e = F(u) & P[u]; e = F(i,u) by A1,A2; hence e in B by A2; end; let e be set; assume e in B; then consider i being Element of I(), u being Element of D() such that A3: e = F(i,u) & P[u]; e = F(u) by A1,A3; hence e in A by A3; 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,YELLOW_4:def 2; "/\"(X,L) <= x by A2,YELLOW_2:24; hence "/\"(X,L) <= y by A3,YELLOW_0:def 2; end; hence "/\"(X,L) <= "/\"(Y,L) 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,YELLOW_4:def 1; "\/"(Y,L) >= y by A2,YELLOW_2:24; hence "\/"(Y,L) >= x by A3,YELLOW_0:def 2; end; hence "\/"(X,L) <= "\/"(Y,L) 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; x in B & y in B by A1,A2,XBOOLE_0:def 3; then consider z being Element of T such that A3: z in B and A4: x <= z and A5: y <= z by WAYBEL_0:def 1; take z; x in A by A1,XBOOLE_0:def 3; then z in A by A4,WAYBEL_0:def 20; hence z in A /\ B by A3,XBOOLE_0:def 3; thus x <= z & y <= z by A4,A5; end; definition let T be reflexive non empty RelStr; cluster non empty directed finite Subset of T; existence proof consider x being 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,LATTICE3:def 9; 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; x >= c & c >= x by A1,A2,A4,A5,LATTICE3:def 9; hence c = x by ORDERS_1:25; end; then ex_sup_of D,T by A2,A3,YELLOW_0:def 7; hence sup D in D by A1,A2,A3,YELLOW_0:def 9; end; definition cluster trivial reflexive transitive non empty antisymmetric with_suprema with_infima finite strict RelStr; existence proof 0 in {0} by TARSKI:def 1; then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:8; reconsider T = RelStr(#{0},r#) as non empty RelStr; take T; thus T is trivial; 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 x <= x by ORDERS_1:def 9; end; then reconsider T' = T as trivial non empty reflexive RelStr; T' is transitive; hence T is transitive; thus T is non empty; T' is antisymmetric; hence T is antisymmetric; T' is with_suprema; hence T is with_suprema; T' is with_infima; hence T is with_infima; thus T is finite by GROUP_1:def 13; thus thesis; end; end; definition cluster finite non empty strict 1-sorted; existence proof take S = 1-sorted(#{{}}#); thus the carrier of S is finite non empty; thus thesis; end; end; definition let T be finite 1-sorted; cluster -> finite Subset of T; coherence proof let S be Subset of T; reconsider C = the carrier of T as finite set by GROUP_1:def 13; S is Subset of C; hence S is finite; end; end; definition let R be RelStr; cluster {}R -> lower upper; coherence proof thus for x,y being Element of R st x in {}R & y <= x holds y in {}R; thus for x,y being Element of R st x in {}R & x <= y holds y in {}R; end; end; definition let R be trivial non empty RelStr; cluster -> upper Subset of R; coherence proof let S be Subset of R; consider x being Element of R such that A1: the carrier of R = {x} by TEX_1:def 1; S = {} or S = the carrier of R by A1,ZFMISC_1:39; then S = {}R or S = [#]R by PRE_TOPC:12; hence S is upper; 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 set 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 YELLOW_6:10; then A` misses downarrow x by Th5; then A` c= (downarrow x)` by PRE_TOPC:21; hence downarrow x c= A by PRE_TOPC:19; 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; synonym S is inaccessible; 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; synonym S is directly_closed; 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; synonym S has_the_property_(S); end; definition let T be non empty reflexive RelStr; cluster {}T -> property(S) directly_closed; coherence proof for D being non empty directed Subset of T st sup D in {}T 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 {}T; hence {}T is property(S) by Def3; thus for D being non empty directed Subset of T st D c= {}T holds sup D in {} T by XBOOLE_1:3; end; end; definition let T be non empty reflexive RelStr; cluster property(S) directly_closed Subset of T; existence proof take {}T; thus thesis; end; end; definition 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 YELLOW_6:10; 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 3; then D meets S by XBOOLE_0:def 7; hence contradiction by A1,PRE_TOPC:21; 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; definition let T be reflexive transitive antisymmetric non empty with_suprema finite RelStr; cluster -> inaccessible 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 D meets S 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 proof thus T is Scott implies for S being Subset of T holds S is open iff S is upper by Def4; assume A1: for S being Subset of T holds S is open iff S is upper; let S be Subset of T; thus S is open iff S is inaccessible upper by A1; end; end; definition cluster trivial complete strict non empty Scott TopLattice; existence proof consider T being trivial reflexive non empty discrete strict finite TopRelStr; take T; thus T is trivial complete strict non empty; let S be Subset of T; thus S is open iff S is upper by TDLAT_3:17; end; end; definition let T be non empty reflexive RelStr; cluster [#]T -> directly_closed inaccessible; coherence proof thus [#]T is directly_closed proof let D be non empty directed Subset of T such that D c= [#]T; thus sup D in [#]T by PRE_TOPC:13; end; let D be non empty directed Subset of T such that sup D in [#]T; consider p being Element of T such that A1: p in D by SUBSET_1:10; p in [#]T by PRE_TOPC:13; hence D meets [#]T by A1,XBOOLE_0:3; end; end; definition let T be non empty reflexive RelStr; cluster directly_closed lower inaccessible upper Subset of T; existence proof take [#]T; thus [#]T is directly_closed lower inaccessible upper; end; end; definition 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 PRE_TOPC:21; then not sup D in S by Def1; hence sup D in S` by YELLOW_6:10; end; end; definition 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 YELLOW_6:10; then not D c= S by Def2; then not D c= S``; hence D meets S` by PRE_TOPC:21; 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 by TOPS_1:29; 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 by TOPS_1:29; 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 proof let b be Element of T; assume b in D; hence b <= x by A1,WAYBEL_0:17; end; then sup D <= x by A2,YELLOW_0:30; hence sup D in downarrow x 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:37; 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:37; hence downarrow x c= C by A4,Th6; end; hence Cl {x} = downarrow x by A1,A2,YELLOW_8:17; 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 x' = x, y' = y as Element of T; A1: Cl {x'} = downarrow x' & Cl {y'} = downarrow y' by Th9; assume x <> y; hence Cl {x} <> Cl {y} by A1,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 proof let T be Scott up-complete (non empty reflexive transitive antisymmetric TopRelStr), x be Element of T; downarrow x is directly_closed lower by Th8; hence downarrow x is closed by Th7; end; 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 (downarrow x)` is open by TOPS_1:29; 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:55; A misses downarrow x by A1,Th5; then A c= (downarrow x)` by PRE_TOPC:21; hence (downarrow x)` is a_neighborhood of A 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 of bool the carrier of T from SubsetD; then F is Subset-Family of T by SETFAM_1:def 7; then reconsider F as Subset-Family of T; take F; thus S = meet F proof [#]T is a_neighborhood of S by YELLOW_6:7; 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 YELLOW_6:8; end; hence S c= meet F by A1,SETFAM_1:6; let x be set 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:4; p <= p; then p in downarrow p by WAYBEL_0:17; hence contradiction by A2,A4,YELLOW_6:10; 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 X is a_neighborhood of S; 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 has_the_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,Def1; then consider y being set 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,WAYBEL_0:def 20; end; end; assume that A6: S is upper and A7: S has_the_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,Def3; y >= y by YELLOW_0:def 1; then y in S by A8,A9; hence D meets S by A8,XBOOLE_0:3; end; hence S is open by A6,Def4; end; definition let T be complete TopLattice; :: p. 100, Remark 1.4 (vi) cluster lower -> property(S) 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:10; 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:24; hence x in S by A1,A2,WAYBEL_0:def 19; end; end; Lm2: for T being non empty reflexive TopRelStr holds [#]T has_the_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:10; take y; thus y in D by A1; let x be Element of T such that x in D & x >= y; thus x in [#]T by PRE_TOPC:13; 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 has_the_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 has_the_property_(S)}; [#]T has_the_property_(S) by Lm2; then [#]T in the topology of T by A1; hence the carrier of T in the topology of T by PRE_TOPC:12; hereby let a be Subset-Family of T such that A2: a c= the topology of T; union a has_the_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 has_the_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,Def3; take y; thus y in D by A7; let u be Element of T; assume u in D & u >= y; then u in X by A8; hence u in union a 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 A9: a = A and A10: A has_the_property_(S) by A1; assume b in the topology of T; then consider B being Subset of T such that A11: b = B and A12: B has_the_property_(S) by A1; A /\ B has_the_property_(S) proof let D be non empty directed Subset of T; assume A13: sup D in A /\ B; then sup D in A by XBOOLE_0:def 3; then consider x being Element of T such that A14: x in D and A15: for z being Element of T st z in D & z >= x holds z in A by A10,Def3; sup D in B by A13,XBOOLE_0:def 3; then consider y being Element of T such that A16: y in D and A17: for z being Element of T st z in D & z >= y holds z in B by A12,Def3; consider z being Element of T such that A18: z in D and A19: x <= z and A20: y <= z by A14,A16,WAYBEL_0:def 1; take z; thus z in D by A18; let u be Element of T such that A21: u in D; assume A22: u >= z; then u >= x by A19,YELLOW_0:def 2; then A23: u in A by A15,A21; u >= y by A20,A22,YELLOW_0:def 2; then u in B by A17,A21; hence u in A /\ B by A23,XBOOLE_0:def 3; end; hence a /\ b in the topology of T by A1,A9,A11; 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 :Def6: "\/"({"/\"({N.i:i >= j},R) where j is Element of N: not contradiction},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 :Def7: 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 Rel_On_Dom_Ex; reconsider C as Convergence-Class of R by YELLOW_6:def 21; 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 p is_S-limit_of N implies [N,p] in C 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 set; A5: it1 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 21; A6: it2 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 21; hereby assume A7: [x,y] in it1; then A8: x in NetUniv R by A5,ZFMISC_1:106; 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 14 ; reconsider p = y as Element of R by A5,A7,ZFMISC_1:106; 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:106; 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 14; reconsider p = y as Element of R by A6,A10,ZFMISC_1:106; p is_S-limit_of N by A4,A10,A11,A12; hence [x,y] in it1 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,WAYBEL_0:def 11; set X = {"/\"({N.i where i is Element of N: i >= j},R) where j is Element of N: not contradiction}; A4: lim_inf N = "\/"(X,R) by Def6; reconsider q'= q, p' = p as Element of R; q' is_>=_than X proof let x be Element of R; assume x in X; then consider j1 being Element of N such that A5: 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 A6: j2 >= j0 & j2 >= j1 by YELLOW_6:def 5; N.j2 in Y by A6; then A7: x <= N.j2 by A5,YELLOW_2:24; N.j2 in downarrow q by A3,A6; then N.j2 <= q' by WAYBEL_0:17; hence x <= q' by A7,YELLOW_0:def 2; end; then lim_inf N <= q' by A4,YELLOW_0:32; then p' <= q' by A1,YELLOW_0:def 2; hence p <= q; 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 by WAYBEL_0:def 11; set X = {"/\"({N.i where i is Element of N: i >= j},R) where j is Element of N: not contradiction}, Y = {N.i where i is Element of N: i >= j0}; A2: lim_inf N = "\/"(X,R) by Def6; reconsider q'= q as Element of R; "/\"(Y,R) in X; then A3: lim_inf N >= "/\"(Y,R) by A2,YELLOW_2:24; q' is_<=_than Y proof let y be Element of R; assume y in Y; then consider i1 being Element of N such that A4: y = N.i1 and A5: i1 >= j0; reconsider i1' = i1 as Element of N; N.i1' in uparrow q by A1,A5; hence q' <= y by A4,WAYBEL_0:18; end; then "/\"(Y,R) >= q' by YELLOW_0:33; hence lim_inf N >= q by A3,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 by WAYBEL_0:def 9; let i,j be Element of N; A2: netmap(N,R).i = (the mapping of N).i by WAYBEL_0:def 7 .= N.i by WAYBEL_0:def 8; A3: netmap(N,R).j = (the mapping of N).j by WAYBEL_0:def 7 .= N.j by WAYBEL_0:def 8; reconsider i' = i, j' = j as Element of N; assume i <= j; then netmap(N,R).i' <= netmap(N,R).j' by A1,WAYBEL_1:def 2; hence N.i <= N.j by A2,A3; end; assume A4: 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; A5: netmap(N,R).x = (the mapping of N).x by WAYBEL_0:def 7 .= N.x by WAYBEL_0:def 8; A6: netmap(N,R).y = (the mapping of N).y by WAYBEL_0:def 7 .= N.y by WAYBEL_0:def 8; assume x <= y; hence netmap(N,R).x <= netmap(N,R).y by A4,A5,A6; end; hence N is monotone by WAYBEL_0:def 9; 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 Rel_On_Dom_Ex; 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; A2: f.y = N.j by WAYBEL_0:def 8; [x,y] in the InternalRel of N iff f.x <= f.y by A1; hence i <= j iff N.i <= N.j by A2,ORDERS_1:def 9,WAYBEL_0:def 8; end; uniqueness proof let it1,it2 be strict non empty NetStr over R such that A3: the carrier of it1 = S and A4: the mapping of it1 = f and A5: for i,j being Element of it1 holds i <= j iff it1.i <= it1.j and A6: the carrier of it2 = S and A7: the mapping of it2 = f and A8: 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 set; hereby assume A9: [x,y] in the InternalRel of it1; then A10: x in S & y in S by A3,ZFMISC_1:106; then reconsider i=x, j=y as Element of it1 by A3; reconsider i'=x, j'=y as Element of it2 by A6,A10; A11: it1.i = f.i by A4,WAYBEL_0:def 8 .= it2.i' by A7,WAYBEL_0:def 8; A12: it1.j = f.j by A4,WAYBEL_0:def 8 .= it2.j' by A7,WAYBEL_0:def 8; i <= j by A9,ORDERS_1:def 9; then it2.i' <= it2.j' by A5,A11,A12; then i' <= j' by A8; hence [x,y] in the InternalRel of it2 by ORDERS_1:def 9; end; assume A13: [x,y] in the InternalRel of it2; then A14: x in S & y in S by A6,ZFMISC_1:106; then reconsider i=x, j=y as Element of it2 by A6; reconsider i'=x, j'=y as Element of it1 by A3,A14; A15: it2.i = f.i by A7,WAYBEL_0:def 8 .= it1.i' by A4,WAYBEL_0:def 8; A16: it2.j = f.j by A7,WAYBEL_0:def 8 .= it1.j' by A4,WAYBEL_0:def 8; i <= j by A13,ORDERS_1:def 9; then it1.i' <= it1.j' by A8,A15,A16; then i' <= j' by A5; hence [x,y] in the InternalRel of it1 by ORDERS_1:def 9; end; hence it1 = it2 by A3,A4,A6,A7; end; end; theorem Th19: for L being non empty 1-sorted, N being non empty NetStr over L holds rng the mapping of N = { N.i where i is Element of N: not contradiction} proof let L be non empty 1-sorted, N be non empty NetStr over L; set X = { N.i where i is Element of N: not contradiction}; A1: the carrier of N = dom the mapping of N by FUNCT_2:def 1; thus rng the mapping of N c= { N.i where i is Element of N: not contradiction} proof let e be set; assume e in rng the mapping of N; then consider u being set such that A2: u in dom the mapping of N and A3: e = (the mapping of N).u by FUNCT_1:def 5; reconsider u as Element of N by A2,FUNCT_2:def 1; e = N.u by A3,WAYBEL_0:def 8; hence e in X; end; let e be set; assume e in X; then consider i being Element of N such that A4: e = N.i; e = (the mapping of N).i by A4,WAYBEL_0:def 8; hence e in rng the mapping of N by A1,FUNCT_1:def 5; 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; A2: f = the mapping of N by Def10; then rng f = { N.i where i is Element of N: not contradiction} by Th19; then N.x in rng f & N.y in rng f; then consider p being Element of R such that A3: p in rng f and A4: N.x <= p & N.y <= p by A1,WAYBEL_0:def 1; consider z being set such that A5: z in dom f and A6: p = f.z by A3,FUNCT_1:def 5; z in the carrier of N by A2,A5,FUNCT_2:def 1; then reconsider z as Element of N; take z; p = N.z by A2,A6,WAYBEL_0:def 8; hence x <= z & y <= z by A4,Def10; end; definition 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 = (the mapping of N).x by WAYBEL_0:def 7 .= N.x by WAYBEL_0:def 8; A2: netmap(N,R).y = (the mapping of N).y by WAYBEL_0:def 7 .= N.y by WAYBEL_0:def 8; assume x <= y; hence netmap(N,R).x <= netmap(N,R).y by A1,A2,Def10; end; hence thesis by WAYBEL_0:def 9; end; end; definition 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 x <= y & y <= z; then N.x <= N.y & N.y <= N.z by Def10; then N.x <= N.z by YELLOW_0:def 2; hence x <= z by Def10; end; end; definition 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; A3: UN = Tarski-Class the_transitive-closure_of the carrier of R by YELLOW_6: def 3; reconsider UN as universal set; A4: the_transitive-closure_of the carrier of R in UN by A3,CLASSES1:5; the carrier of R c= the_transitive-closure_of the carrier of R by CLASSES1:59; then the carrier of R in UN by A3,A4,CLASSES1:6; then A5: S in UN by A1,CLASSES1:def 1; the carrier of N = S by Def10; hence Net-Str(S,f) in NetUniv R by A5,YELLOW_6:def 14; end; definition let R be LATTICE; cluster monotone reflexive strict 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 = the carrier of R by RELAT_1:71 .= [#]R by PRE_TOPC:12; then reconsider N = Net-Str(the carrier of R,f) as strict reflexive net of R by Th20; take N; thus thesis; end; end; 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; defpred P[set] means not contradiction; 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 j' = j as Element of N; j' <= j'; then N.j' in Y; hence N.j >= b by A3,LATTICE3:def 8; end; hence N.j = "/\"(Y,R) 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 FraenkelF'(A1); hence lim_inf N = "\/"(rng the mapping of N,R) by Def6 .= 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 = {"/\"({N.i where i is Element of N: i >= j},R) where j is Element of N: not contradiction}; consider j being 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 5; 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:25 .= N.j by YELLOW_6:25; hence N.j >= b by A2,A4,YELLOW_2:24; 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,LATTICE3:def 9; 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:25 .= N.i0 by YELLOW_6:25; 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 5; A11: N.i0 in Y by A10; assume A12: c is_<=_than Y; N.j = the_value_of N by YELLOW_6:25 .= N.i0 by YELLOW_6:25; hence N.j >= c by A11,A12,LATTICE3:def 8; end; hence N.j <= b by A7,A8,YELLOW_0:33; end; thus the_value_of N = N.j by YELLOW_6:25 .= "\/"(X,R) by A1,A5,YELLOW_0:32 .= lim_inf N by Def6; end; theorem Th24: for R being complete LATTICE, N being constant net of R holds the_value_of N is_S-limit_of N proof let R be complete LATTICE, N be constant net of R; the_value_of N <= lim_inf N by Th23; hence the_value_of N is_S-limit_of N by Def7; end; 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:8; dom id{e} = {e} & rng id{e} = {e} by RELAT_1:71; then reconsider f = id{e} as Function of {e}, the carrier of S by FUNCT_2:def 1,RELSET_1:11; take NetStr(#{e},r,f#); thus thesis; end; uniqueness; end; definition 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; x in the carrier 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: x in the carrier of Net-Str e & the carrier of Net-Str e = {e} by Def11; then A2: x = e by TARSKI:def 1; thus N.x = (the mapping of N).x by WAYBEL_0:def 8 .= (id{e}).x by Def11 .= e by A1,A2,FUNCT_1:35; end; definition 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; A1: the carrier of N = {e} by Def11; e in {e} by TARSKI:def 1; then reconsider e as Element of N by A1; the InternalRel of N = {[e,e]} by Def11; then A2: [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 x <= x by A2,ORDERS_1:def 9; end; thus N is transitive proof let x,y,z be Element of N such that x <= y & y <= z; x = e & z = e by Th25; hence thesis by A2,ORDERS_1:def 9; end; thus N is directed proof let x,y be Element of N; take e; x = e & y = e by Th25; hence thesis by A2,ORDERS_1:def 9; end; let x,y be Element of N such that x <= y & y <= x; x = e & y = e by Th25; hence thesis; 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; A1: the carrier of N = {e} by Def11; e in {e} by TARSKI:def 1; then reconsider d = e as Element of N by A1; hereby assume N is_eventually_in X; then consider x being Element of N such that A2: for y being Element of N st x <= y holds N.y in X by WAYBEL_0:def 11; N.x in X by A2; hence e in X by Th26; end; assume A3: e in X; take d; let j be Element of N such that d <= j; thus N.j in X by A3,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 = {"/\"({N.i where i is Element of N: i >= j},S) where j is Element of N: not contradiction}; reconsider e' = e as Element of S; A1: X c= {e'} proof let u be set; 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= {e'} proof let v be set; assume v in Y; then consider i being Element of N such that A4: v = N.i and i >= j; reconsider i' = i as Element of N; N.i' = e by Th26; hence v in {e'} by A4,TARSKI:def 1; end; reconsider j' = j as Element of N; j' <= j'; then N.j in Y; then Y = {e'} by A3,ZFMISC_1:39; then u = e' by A2,YELLOW_0:39; hence u in {e'} by TARSKI:def 1; end; consider j being Element of N; "/\"({N.i where i is Element of N: i >= j},S) in X; then X = {e'} by A1,ZFMISC_1:39; hence e = "\/"(X,S) by YELLOW_0:39 .= lim_inf Net-Str e by Def6; 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} & e in the carrier of S by Def11; A2: UN = Tarski-Class the_transitive-closure_of the carrier of S by YELLOW_6: def 3; reconsider UN as universal set; A3: the_transitive-closure_of the carrier of S in UN by A2,CLASSES1:5; the carrier of S c= the_transitive-closure_of the carrier of S by CLASSES1:59; then the carrier of S in UN by A2,A3,CLASSES1:6; then the carrier of N in the_universe_of the carrier of S by A1,CLASSES1:def 1; hence Net-Str e in NetUniv S by YELLOW_6:def 14; end; theorem Th30: for R being complete LATTICE, Z be net of R, D be Subset of R st D = {"/\"({Z.k where k is Element of Z: k >= j},R) where j is Element of Z: not contradiction} 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 = {"/\"({Z.k where k is Element of Z: k >= j},R) where j is Element of Z: not contradiction}; consider j being 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 5; 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 set; 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 e in E1 by A6; end; hence x <= z by A2,WAYBEL_7:3; E c= Ey proof let e be set; 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 e in Ey by A8; end; hence y <= z by A3,WAYBEL_7:3; 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 27; let S be Subset of L; hereby assume S in the topology of T; then consider V being Subset of L such that A2: S = V and A3: 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 A4: sup D in S; A5: dom id D = D & rng id D = D by RELAT_1:71; then reconsider f = id D as Function of D, the carrier of L by FUNCT_2:def 1,RELSET_1:11; 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:71; then sup D is_S-limit_of N by Def7; then [N,sup D] in SC by A6,Def8; then N is_eventually_in S by A2,A3,A4; then consider i0 being Element of N such that A7: for j being Element of N st i0 <= j holds N.j in S by WAYBEL_0:def 11; consider j0 being Element of N such that A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def 5; A9: N.j0 in S by A7,A8; A10: D = the carrier of N by Def10; N.j0 = (the mapping of N).j0 by WAYBEL_0:def 8 .= (id D).j0 by Def10 .= j0 by A10,FUNCT_1:35; hence D meets S 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,Def7; then [Net-Str y,x] in SC by A13,Def8; then Net-Str y is_eventually_in S by A2,A3,A11; hence y in S 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 p' = 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 21; then A18: N in NetUniv L by A17,ZFMISC_1:106; then ex N' being strict net of L st N' = N & the carrier of N' in the_universe_of the carrier of L by YELLOW_6:def 14; then p is_S-limit_of N by A17,A18,Def8; then A19: p' <= lim_inf N by Def7; defpred P[set] means not contradiction; 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 SubsetFD; then reconsider D = X as Subset of L; reconsider D as non empty directed Subset of L by Th30; lim_inf N = sup D by Def6; then sup D in S by A15,A16,A19,WAYBEL_0:def 20; then D meets S by A14,Def1; then D /\ S <> {} by XBOOLE_0:def 7; then consider d being Element of L such that A20: d in D /\ S by SUBSET_1:10; reconsider d as Element of L; d in D by A20,XBOOLE_0:def 3; 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 3; 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:24; hence N.i0 in S by A15,A22,WAYBEL_0:def 20; end; hence S in the topology of T 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; A1: the carrier of T = the carrier of CSC by YELLOW_6:def 27; the topology of T = the topology of CSC proof thus the topology of T c= the topology of CSC proof let e be set; assume A2: e in the topology of T; then reconsider A = e as Subset of T; A is open by A2,PRE_TOPC:def 5; then A is inaccessible upper by Def4; hence e in the topology of CSC by Th31; end; let e be set; assume A3: e in the topology of CSC; then reconsider A = e as Subset of T by A1; A is inaccessible upper by A3,Th31; then A is open by Def4; hence e in the topology of T by PRE_TOPC:def 5; end; hence the TopStruct of T = ConvergenceSpace Scott-Convergence T by YELLOW_6:def 27; 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 27; let S be Subset of T; hereby assume S is open; then S in the topology of T by PRE_TOPC:def 5; then consider V being Subset of T such that A2: S = V and A3: 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 A4: sup D in S; A5: dom id D = D & rng id D = D by RELAT_1:71; then reconsider f = id D as Function of D, the carrier of T by FUNCT_2:def 1,RELSET_1:11; 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:71; then sup D is_S-limit_of N by Def7; then [N,sup D] in SC by A6,Def8; then N is_eventually_in S by A2,A3,A4; then consider i0 being Element of N such that A7: for j being Element of N st i0 <= j holds N.j in S by WAYBEL_0:def 11; consider j0 being Element of N such that A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def 5; A9: N.j0 in S by A7,A8; A10: D = the carrier of N by Def10; N.j0 = (the mapping of N).j0 by WAYBEL_0:def 8 .= (id D).j0 by Def10 .= j0 by A10,FUNCT_1:35; hence D meets S 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,Def7; then [Net-Str y,x] in SC by A13,Def8; then Net-Str y is_eventually_in S by A2,A3,A11; hence y in S 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 p' = 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 21; then A18: N in NetUniv T by A17,ZFMISC_1:106; then ex N' being strict net of T st N' = N & the carrier of N' in the_universe_of the carrier of T by YELLOW_6:def 14; then p is_S-limit_of N by A17,A18,Def8; then A19: p' <= lim_inf N by Def7; defpred P[set] means not contradiction; 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 SubsetFD; then reconsider D = X as Subset of T; reconsider D as non empty directed Subset of T by Th30; lim_inf N = sup D by Def6; then sup D in S by A15,A16,A19,WAYBEL_0:def 20; then D meets S by A14,Def1; then D /\ S <> {} by XBOOLE_0:def 7; then consider d being Element of T such that A20: d in D /\ S by SUBSET_1:10; reconsider d as Element of T; d in D by A20,XBOOLE_0:def 3; 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 3; 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:24; hence N.i0 in S by A15,A22,WAYBEL_0:def 20; end; then S in the topology of T by A1; hence S is open by PRE_TOPC:def 5; end; theorem Th34: for T being complete TopLattice st the TopStruct of T = ConvergenceSpace Scott-Convergence T holds T is Scott proof let T be complete TopLattice; assume the TopStruct of T = ConvergenceSpace Scott-Convergence T; hence for S being Subset of T holds S is open iff S is inaccessible upper by Th33; end; definition 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 14; the_value_of M is_S-limit_of M by A2,Th24; hence [N,the_value_of N] in Scott-Convergence R by A1,A2,Def8; end; end; definition 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 21; assume A2: Y in NetUniv R; then consider Y' being strict net of R such that A3: Y' = Y and the carrier of Y' in the_universe_of the carrier of R by YELLOW_6:def 14; let p be Element of R; reconsider p' = p as Element of R; assume A4: [N,p] in S; then A5: N in NetUniv R by A1,ZFMISC_1:106; then consider N' being strict net of R such that A6: N' = N and the carrier of N' in the_universe_of the carrier of R by YELLOW_6:def 14; deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R); defpred P[set] means not contradiction; reconsider X1 = {F(j) where j is Element of N: P[j]} as Subset of R from SubsetFD; 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 SubsetFD; p is_S-limit_of N' by A4,A5,A6,Def8; then p <= lim_inf N by A6,Def7; then A7: p' <= "\/"(X1,R) by Def6; consider f being map 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 12; 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 set; 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 = ((the mapping of N)*f).m by A8,A12,WAYBEL_0:def 8 .= (the mapping of N).(f.m) by FUNCT_2:21 .= N.(f.m) by WAYBEL_0:def 8; hence u in X4 by A14; end; hence a <= b by A10,WAYBEL_7:3; end; then "\/"(X1,R) <= "\/"(X2,R) by Th2; then p' <= "\/"(X2,R) by A7,YELLOW_0:def 2; then p <= lim_inf Y by Def6; then p is_S-limit_of Y' by A3,Def7; hence [Y,p] in S 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 13; then A2: (the mapping of N).j in X by FUNCT_1:def 13; the mapping of M = (the mapping of N)|the carrier of M by A1,YELLOW_6:def 8 ; then (the mapping of M).j in X by A2,FUNCT_1:72; hence M.j in X by WAYBEL_0:def 8; end; definition let L be non empty reflexive RelStr; func sigma L -> Subset-Family of L equals :Def12: the topology of ConvergenceSpace Scott-Convergence L; coherence by YELLOW_6:def 27; 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:54; d in W by A2,WAYBEL_3:8; hence D meets W by A1,XBOOLE_0:3; end; hence wayabove x is open 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; A1: sigma T = the topology of ConvergenceSpace Scott-Convergence T by Def12; 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 A1,YELLOW_6:def 27; 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 proof let T1,T2 be TopStruct such that A1: the TopStruct of T1 = the TopStruct of T2 and A2: T1 is TopSpace-like; thus the carrier of T2 in the topology of T2 by A1,A2,PRE_TOPC:def 1; thus (for a being Subset-Family of T2 st a c= the topology of T2 holds union a in the topology of T2) & (for a,b being Subset of T2 st a in the topology of T2 & b in the topology of T2 holds a /\ b in the topology of T2) by A1,A2,PRE_TOPC:def 1; end; 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 proof let S1,S2 be non empty 1-sorted such that A1: the carrier of S1 = the carrier of S2; let N be strict net of S1; reconsider M = N as net of S2 by A1; A2: the carrier of N = the carrier of M & the InternalRel of N = the InternalRel of M & the mapping of N = the mapping of M; M = the NetStr of N .= the NetStr of M by A2; hence N is strict net of S2; end; 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 & the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def 14; reconsider N as strict net of S2 by A1,Lm4; thus P[x] proof take N; thus thesis by A1,A3; end; end; assume P[x]; then consider N being strict net of S2 such that A4: N = x & the carrier of N in the_universe_of the carrier of S2; reconsider N as strict net of S1 by A1,Lm4; now take N; thus N = x & the carrier of N in the_universe_of the carrier of S1 by A1,A4; end; hence x in NetUniv S1 by YELLOW_6:def 14; end; A5: for x being set holds x in NetUniv S2 iff P[x] by YELLOW_6:def 14; thus NetUniv S1 = NetUniv S2 from Extensionality(A2,A5); end; Lm6: for T1,T2 being non empty 1-sorted, X be set st the carrier of T1 = the carrier of T2 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 such that the carrier of T1 = the carrier of T2; 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 by WAYBEL_0:def 11; 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 = (the mapping of N2).jj by WAYBEL_0:def 8 .= (the mapping of N1).j by A1 .= N1.j by WAYBEL_0:def 8; hence N2.jj in X 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:54; reconsider H = G as Subset of T1 by A1; G in the topology of T2 by A5,PRE_TOPC:def 5; then H is open by A1,PRE_TOPC:def 5; then p1 in Int W by A3,A6,A7,TOPS_1:54; 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 18; then consider i being Element of N1 such that A8: for j being Element of N1 st i <= j holds N1.j in W by WAYBEL_0:def 11; 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 = (the mapping of N2).jj by WAYBEL_0:def 8 .= (the mapping of N1).j by A2 .= N1.j by WAYBEL_0:def 8; hence N2.jj in V by A2,A8,A9; end; end; hence p2 in Lim N2 by YELLOW_6:def 18; 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 21; A3: Convergence T2 c= [:NetUniv T2,the carrier of T2:] by YELLOW_6:def 21; let u1,u2 be set; 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:9; 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 14; then reconsider N1 as net of T1; A7: p1 in Lim N1 by A4,A5,YELLOW_6:def 22; reconsider N2 = N1 as net of T2 by A1; reconsider p2 =p1 as Point of T2 by A1; N2 in NetUniv T2 & p2 in Lim N2 by A1,A6,A7,Lm5,Lm7; hence [u1,u2] in Convergence T2 by A5,YELLOW_6:def 22; end; assume A8: [u1,u2] in Convergence T2; then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that A9: [u1,u2] = [N1,p1] by A3,DOMAIN_1:9; A10: 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 14; then reconsider N1 as net of T2; A11: p1 in Lim N1 by A8,A9,YELLOW_6:def 22; reconsider N2 = N1 as net of T1 by A1; reconsider p2 =p1 as Point of T1 by A1; N2 in NetUniv T1 & p2 in Lim N2 by A1,A10,A11,Lm5,Lm7; hence [u1,u2] in Convergence T1 by A9,YELLOW_6:def 22; 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 x' = x, y' = y as Element of R1 by A1; consider z' being Element of R1 such that A4: z' <= x' & z' <= y' and A5: for w' being Element of R1 st w' <= x' & w' <= y' holds w' <= z' by A2,LATTICE3:def 11; reconsider z = z' as Element of R2 by A1; take z; thus z <= x & z <= y by A1,A4,Lm1; let w be Element of R2; reconsider w' = w as Element of R1 by A1; assume w <= x & w <= y; then w' <= x' & w' <= y' by A1,Lm1; then w' <= z' by A5; hence w <= z by A1,Lm1; end; A6: R2 is with_suprema proof let x,y be Element of R2; reconsider x' = x, y' = y as Element of R1 by A1; consider z' being Element of R1 such that A7: z' >= x' & z' >= y' and A8: for w' being Element of R1 st w' >= x' & w' >= y' holds w' >= z' by A2,LATTICE3:def 10; reconsider z = z' as Element of R2 by A1; take z; thus z >= x & z >= y by A1,A7,Lm1; let w be Element of R2; reconsider w' = w as Element of R1 by A1; assume w >= x & w >= y; then w' >= x' & w' >= y' by A1,Lm1; then w' >= z' by A8; hence w >= z by A1,Lm1; end; A9: R2 is reflexive proof let x be Element of R2; reconsider x' = x as Element of R1 by A1; x' <= x' by A2,YELLOW_0:def 1; hence x <= x by A1,Lm1; end; A10: R2 is transitive proof let x,y,z be Element of R2; reconsider x' = x, y' = y, z' = z as Element of R1 by A1; assume x <= y & y <= z; then x' <= y' & y' <= z' by A1,Lm1; then x' <= z' by A2,YELLOW_0:def 2; hence x <= z by A1,Lm1; end; R2 is antisymmetric proof let x,y be Element of R2; reconsider x' = x, y' = y as Element of R1 by A1; assume x <= y & y <= x; then x' <= y' & y' <= x' by A1,Lm1; hence x = y by A2,YELLOW_0:def 3; end; hence thesis by A3,A6,A9,A10; 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 proof let R1,R2 be LATTICE, X be set such that A1: the RelStr of R1 = the RelStr of R2; let p1 be Element of R1, p2 be Element of R2 such that A2: p1 = p2 and A3: X is_<=_than p1; let b2 be Element of R2; reconsider b1 = b2 as Element of R1 by A1; assume b2 in X; then p1 >= b1 by A3,LATTICE3:def 9; hence p2 >= b2 by A1,A2,Lm1; end; 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 proof let R1,R2 be LATTICE, X be set such that A1: the RelStr of R1 = the RelStr of R2; let p1 be Element of R1, p2 be Element of R2 such that A2: p1 = p2 and A3: X is_>=_than p1; let b2 be Element of R2; reconsider b1 = b2 as Element of R1 by A1; assume b2 in X; then p1 <= b1 by A3,LATTICE3:def 8; hence p2 <= b2 by A1,A2,Lm1; end; 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 a' = a as Element of R1 by A1; assume D is_<=_than a; then D is_<=_than a' by A1,Lm10; then a' >= "\/"(D,R1) by A3,YELLOW_0:def 9; hence a >= b by A1,Lm1; end; hence "\/"(D,R1) = "\/"(D,R2) 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 a' = a as Element of R1 by A1; assume D is_>=_than a; then D is_>=_than a' by A1,Lm11; then a' <= "/\"(D,R1) by A3,YELLOW_0:def 10; hence a <= b by A1,Lm1; end; hence "/\"(D,R1) = "/\"(D,R2) 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, D' being Subset of R2 st D = D' & D is directed holds D' 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, D' be Subset of R2 such that A2: D = D' and A3: D is directed; let x2,y2 be Element of R2 such that A4: x2 in D' & y2 in D'; reconsider x1 = x2, y1 = y2 as Element of R1 by A1; consider z1 being Element of R1 such that A5: z1 in D and A6: x1 <= z1 & y1 <= z1 by A2,A3,A4,WAYBEL_0:def 1; reconsider z2 = z1 as Element of R2 by A1; take z2; thus z2 in D' by A2,A5; thus x2 <= z2 & y2 <= z2 by A1,A6,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 p',q' being Element of R2 st p = p' & q = q' holds p' << q' 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 p',q' be Element of R2 such that A3: p = p' & q = q'; let D' be non empty directed Subset of R2 such that A4: q' <= sup D'; reconsider D = D' as non empty Subset of R1 by A1; reconsider D as non empty directed Subset of R1 by A1,Lm14; sup D = sup D' by A1,Lm12; then q <= sup D by A1,A3,A4,Lm1; then consider d be Element of R1 such that A5: d in D & p <= d by A2,WAYBEL_3:def 1; reconsider d' = d as Element of R2 by A1; take d'; thus d' in D' by A5; thus p' <= d' by A1,A3,A5,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 = {"/\"({N1.i where i is Element of N1: i >= j},R1) where j is Element of N1: not contradiction}, X2 = {"/\"({N2.i where i is Element of N2: i >= j},R2) where j is Element of N2: not contradiction}; A3: X1 = X2 proof thus X1 c= X2 proof let e be set; assume e in X1; then consider j1 being Element of N1 such that A4: 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 set; assume u in Y1; then consider i1 being Element of N1 such that A5: u = N1.i1 and A6: j1 <= i1; reconsider i2 = i1 as Element of N2 by A2; N2.i2 = (the mapping of N2).i2 by WAYBEL_0:def 8 .= (the mapping of N1).i1 by A2 .= u by A5,WAYBEL_0:def 8; hence u in Y2 by A2,A6; end; let u be set; assume u in Y2; then consider i2 being Element of N2 such that A7: u = N2.i2 and A8: j2 <= i2; reconsider i1 = i2 as Element of N1 by A2; N1.i1 = (the mapping of N1).i1 by WAYBEL_0:def 8 .= (the mapping of N2).i2 by A2 .= u by A7,WAYBEL_0:def 8; hence u in Y1 by A2,A8; end; then e = "/\"(Y2,R2) by A1,A4,Lm13; hence e in X2; end; let e be set; assume e in X2; then consider j1 being Element of N2 such that A9: 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 set; assume u in Y1; then consider i1 being Element of N2 such that A10: u = N2.i1 and A11: j1 <= i1; reconsider i2 = i1 as Element of N1 by A2; N1.i2 = (the mapping of N1).i2 by WAYBEL_0:def 8 .= (the mapping of N2).i1 by A2 .= u by A10,WAYBEL_0:def 8; hence u in Y2 by A2,A11; end; let u be set; assume u in Y2; then consider i2 being Element of N1 such that A12: u = N1.i2 and A13: j2 <= i2; reconsider i1 = i2 as Element of N2 by A2; N2.i1 = (the mapping of N2).i1 by WAYBEL_0:def 8 .= (the mapping of N1).i2 by A2 .= u by A12,WAYBEL_0:def 8; hence u in Y1 by A2,A13; end; then e = "/\"(Y2,R1) by A1,A9,Lm13; hence e in X1; end; thus lim_inf N1 = "\/"(X1,R1) by Def6 .= "\/"(X2,R2) by A1,A3,Lm12 .= lim_inf N2 by Def6; end; Lm17: 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, 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 such that the RelStr of R1 = the RelStr of R2; 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 16; A4: the RelStr of Iterated J2 = [:N2, product J2:] by YELLOW_6:def 16; then A5: the carrier of Iterated J1 = the carrier of Iterated J2 by A1,A2,A3; A6: the InternalRel of Iterated J1 = the InternalRel of Iterated J2 by A1,A2,A3,A4; set f = the mapping of Iterated J1, g = the mapping of Iterated J2; A7: 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 set st x in dom f holds f.x = g.x proof let x be set; assume x in dom f; then x in the carrier of Iterated J1 by FUNCT_2:def 1; 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 A8: x = [x1,x2] by DOMAIN_1:9; 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 A8,BINOP_1:def 1 .= (the mapping of J1.x1).(x2.x1) by YELLOW_6:def 16 .= (the mapping of J2.y1).(y2.y1) by A2 .= (the mapping of Iterated J2).(y1,y2) by YELLOW_6:def 16 .= g.x by A8,BINOP_1:def 1; end; then A9: f = g by A7,FUNCT_1:9; thus Iterated J1 = NetStr(#the carrier of Iterated J1, the InternalRel of Iterated J1, the mapping of Iterated J1#) .= NetStr(#the carrier of Iterated J2, the InternalRel of Iterated J2, the mapping of Iterated J2#) by A5,A6,A9 .= Iterated J2; 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 15; N is NetStr over R2 by A1; hence i is net of R2; end; hence J1 is net_set of the carrier of N2,R2 by YELLOW_6:def 15; 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 21; for e being set st e in Scott-Convergence R1 holds e in Scott-Convergence R2 proof let e be set; 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:9; A5: N1 in NetUniv R1; consider N being strict net of R1 such that A6: N1 = N and the carrier of N in the_universe_of the carrier of R1 by YELLOW_6:def 14; reconsider N2 = N1 as strict net of R2 by A1,A6,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 by Def7; then p2 <= lim_inf N2 by A1,A8,Lm1; then p2 is_S-limit_of N2 by Def7; hence e in Scott-Convergence R2 by A4,A7,Def8; end; hence Scott-Convergence R1 c= Scott-Convergence R2 by TARSKI:def 3; end; Lm20: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2 holds Scott-Convergence R1 = Scott-Convergence R2 proof let R1,R2 be complete LATTICE; assume A1: the RelStr of R1 = the RelStr of R2; then A2: Scott-Convergence R1 c= Scott-Convergence R2 by Lm19; Scott-Convergence R2 c= Scott-Convergence R1 by A1,Lm19; hence thesis by A2,XBOOLE_0:def 10; end; 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 27; 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 27; the topology of T1 = the topology of T2 proof thus the topology of T1 c= the topology of T2 proof let e be set; 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; then N1 is_eventually_in V1 by A5,A6; hence N2 is_eventually_in V2 by A1,Lm6; end; hence e in the topology of T2 by A3,A4; end; let e be set; 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; then N1 is_eventually_in V1 by A8,A9; hence N2 is_eventually_in V2 by A1,Lm6; end; hence e in the topology of T1 by A2,A7; end; hence sigma R1 = the topology of T2 by Def12 .= sigma R2 by Def12; 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,LATTICE3:def 12; 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; then a1 <= b1 by A4; hence a2 <= b2 by A1,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 R1 is continuous; then A2: R1 is satisfying_axiom_of_approximation by WAYBEL_3:def 6; thus A3: for x being Element of R2 holds waybelow x is non empty directed; thus R2 is up-complete; A4: for x being Element of R1 holds waybelow x is non empty directed; 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 A5: u1 << x1 and A6: not u1 <= y1 by A2,A4,WAYBEL_3:24; reconsider u2 = u1 as Element of R2 by A1; take u2; thus u2 << x2 by A1,A5,Lm15; thus not u2 <= y2 by A1,A6,Lm1; end; hence R2 is satisfying_axiom_of_approximation by A3,WAYBEL_3:24; end; definition 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 p' = 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 14; not p is_S-limit_of N by A1,A2,A4,Def8; then not p <= lim_inf X by A4,Def7; then consider u being Element of R such that A5: u << p' 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 = {"/\"({X.k where k is Element of X: k >= j},R) where j is Element of X: not contradiction}; A7: lim_inf X = "\/"(C,R) by Def6; "/\"(B,R) in C; then "/\"(B,R) <= lim_inf X by A7,YELLOW_2:24; 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 A8: b in B and A9: not u <= b by LATTICE3:def 8; consider j being Element of X such that A10: b = X.j and A11: j >= i by A8; take j; thus i <= j by A11; thus X.j in A by A9,A10; end; then reconsider Y = X"A as subnet of X by YELLOW_6:31; take Y; reconsider UN = the_universe_of the carrier of R as universal set; A12: ex N being strict net of R st X = N & the carrier of N in UN by A1,YELLOW_6:def 14; X"A is SubRelStr of X by YELLOW_6:def 8; then the carrier of X"A c= the carrier of X by YELLOW_0:def 13; then the carrier of Y in UN by A12,CLASSES1:def 1; hence Y in NetUniv R by YELLOW_6:def 14; let Z be subnet of Y; assume A13: [Z,p] in C; C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 21; then A14: Z in NetUniv R by A13,ZFMISC_1:106; then consider ZZ being strict net of R such that A15: ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def 14; deffunc F(Element of Z) = "/\"({Z.i where i is Element of Z: i >= $1},R); defpred P[set] means not contradiction; set D = {F(j) where j is Element of Z: P[j]}; D is Subset of R from SubsetFD; then reconsider D as Subset of R; reconsider D as non empty directed Subset of R by Th30; A16: lim_inf Z = sup D by Def6; p is_S-limit_of ZZ by A13,A14,A15,Def8; then p <= lim_inf Z by A15,Def7; then consider d being Element of R such that A17: d in D and A18: u <= d by A5,A16,WAYBEL_3:def 1; consider j being Element of Z such that A19: d = "/\"({Z.k where k is Element of Z: k >= j},R) by A17; reconsider j' = j as Element of Z; consider i being Element of Z such that A20: i >= j' & i >= j' by YELLOW_6:def 5; consider f being map of Z, Y such that A21: 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 12; Z.i in {Z.k where k is Element of Z: k >= j} by A20; then A22: d <= Z.i by A19,YELLOW_2:24; Y.(f.i) = (the mapping of Y).(f.i) by WAYBEL_0:def 8 .= ((the mapping of Y)*f).i by FUNCT_2:21 .= Z.i by A21,WAYBEL_0:def 8; then Z.i in A by Th35; then ex a being Element of R st a = Z.i & not a >= u; hence contradiction by A18,A22,YELLOW_0:def 2; end; thus C is (ITERATED_LIMITS) proof let X be net of R, p be Element of R such that A23: [X,p] in C; let J be net_set of the carrier of X, R such that A24: for i being Element of X holds [J.i,X.i] in C; A25: C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 21; then A26: X in NetUniv R by A23,ZFMISC_1:106; 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 A24; hence J.i in NetUniv R by A25,ZFMISC_1:106; end; then A27: Iterated J in NetUniv R by A26,YELLOW_6:34; reconsider p' = p as Element of R; set q = lim_inf Iterated J; q is_>=_than waybelow p' proof let u be Element of R; assume u in waybelow p'; then A28: u << p' by WAYBEL_3:7; set T = TopRelStr(#the carrier of R,the InternalRel of R, sigma R#); A29: the RelStr of T = the RelStr of R; the carrier of R = the carrier of ConvergenceSpace C by YELLOW_6:def 27; then A30: the TopStruct of T = the TopStruct of ConvergenceSpace C by Def12; then reconsider T as TopLattice by A29,Lm3,Lm9; reconsider T as complete TopLattice by A29,Lm22; reconsider T as continuous complete TopLattice by A29,Lm23; the topology of T = sigma T by A29,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 A29,Lm18; reconsider uu = u, qq = q, pp = p' as Element of T ; set N = Iterated JJ; set CC = Convergence T; CC = Convergence ConvergenceSpace C by A30,Lm8; then A31: C c= CC by YELLOW_6:49; A32: uu << pp by A28,A29,Lm15; N = Iterated J by A29,Lm17; then A33: qq = lim_inf N by A29,Lm16; 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; A34: X.ii = (the mapping of X).ii by WAYBEL_0:def 8 .= (the mapping of XX).i .= XX.i by WAYBEL_0:def 8; [J.ii,X.ii] in C by A24; hence [JJ.i,XX.i] in CC by A31,A34; end; then [N,pp] in CC by A23,A31,YELLOW_6:def 26; then A35: pp in Lim N by YELLOW_6:def 22; A36: wayabove uu is open by Th36; pp in wayabove uu by A32,WAYBEL_3:8; then wayabove uu is a_neighborhood of pp by A36,CONNSP_2:5; then A37: N is_eventually_in wayabove uu by A35,YELLOW_6:def 18; wayabove uu c= uparrow uu by WAYBEL_3:11; then N is_eventually_in uparrow uu by A37,WAYBEL_0:8; then uu <= qq by A33,Th18; hence u <= q by A29,Lm1; end; then sup waybelow p' <= q by YELLOW_0:32; then p <= q by WAYBEL_3:def 5; then p is_S-limit_of Iterated J by Def7; hence [Iterated J,p] in C by A27,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:53; 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 14 ; 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 x in Lim N by YELLOW_6:def 22; end; assume x in Lim N; then [M,x] in Scott-Convergence T by A1,A2,A3,A4,YELLOW_6:def 22; hence x is_S-limit_of N 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; reconsider r = [:I,I:] as Relation of I by RELSET_1:def 1; dom F = I by PBOOLE:def 3; 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:106; hence i <= j by ORDERS_1:def 9; end; A7: X is transitive proof let x,y,z be Element of X such that x <= y & y <= z; thus x <= z by A6; end; X is directed proof let x,y be Element of X; take x; thus x <= x & y <= x 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 LambdaDMS; 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 i' = i as Element of I; reconsider rFi = rng(F.i') as Subset of L; A9: rFi is directed by A4; J.i' = Net-Str(K.i',F.i') by A8; hence J.i is net of L by A9,Th20; end; then reconsider J as net_set of the carrier of X, L by YELLOW_6:33; 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 i' = i as Element of I; take R = Net-Str(K.i',F.i'); thus R = J.i by A8; thus K.i = the carrier of R 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 PBOOLE:def 3; 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 i' = i as Element of I; A15: J.i = Net-Str(K.i',F.i') by A8; then reconsider Ji = J.i as strict net of L; K.i' 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 J.i in NetUniv L by YELLOW_6:def 14; end; A16: for i being Element of X holds [J.i,X.i] in C proof let i be Element of X; reconsider i' = i as Element of I; A17: J.i = Net-Str(K.i',F.i') 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 A19: i' in dom F by PBOOLE:def 3; X.i = (Sups F).i by WAYBEL_0:def 8 .= Sup(F.i') by A19,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 by Def7; hence [J.i,X.i] in C by A17,A18,Def8; end; A20: X in NetUniv L by A2,YELLOW_6:def 14; then A21: Iterated J in NetUniv L by A14,YELLOW_6:34; 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:35; 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}; defpred P[set] means not contradiction; 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 = {"/\"(I(j),L) where j is Element of Iterated J: not contradiction}; set D' = {F(i,g) where i is Element of X, g is Element of product doms F: P[g]}; set E' = {F(g) where g is Element of product doms F : P[g]}; A22: 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 set holds y in I(j,g) iff ex x being set st x in dom((Frege F).g) & y = ((Frege F).g).x proof let y be set; g in product Carrier J by A11; then A23: 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 A24: y =G.(i,g) and i >= j; reconsider x = i as set; take x; reconsider i' = i as Element of I; i in I; then A25: i' in dom F by PBOOLE:def 3; hence x in dom((Frege F).g) by A12,WAYBEL_5:8; thus ((Frege F).g).x = F.i'.(g.i) by A12,A25,WAYBEL_5:9 .= (the mapping of Net-Str(K.i',F.i')).(g.i) by Def10 .= (the mapping of J.i).(g.i) by A8 .= y by A23,A24,YELLOW_6:def 16; end; given x being set 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; then reconsider i' = x as Element of I by PBOOLE:def 3; reconsider i = i' 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.i',F.i')).(g.i) by Def10 .= (the mapping of J.i).(g.i) by A8 .= G.(i,g) by A23,YELLOW_6:def 16; hence y in I(j,g) by A29; end; hence "/\"(rng((Frege F).g),L) = "/\"(I(j,g),L) by FUNCT_1:def 5; end; A30: D = D' proof A31: the carrier of Iterated J = [:the carrier of X, product Carrier J:] by YELLOW_6:35; 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 16; g in product Carrier J by A11; then g in the carrier of product J by YELLOW_1:def 4; then reconsider g' = g as Element of product J; g' in the carrier of product J; then A35: g' in product Carrier J by YELLOW_1:def 4; reconsider i' = i as Element of X; for i be set st i in the carrier of X ex R being RelStr, xi,yi being Element of R st R = J.i & xi = g'.i & yi = g'.i & xi <= yi proof let i be set; assume i in the carrier of X; then reconsider ii = i as Element of X; reconsider i' = ii as Element of I; A36: J.i = Net-Str(K.i',F.i') by A8; set R = Net-Str(K.i',F.i'); g'.ii in the carrier of R by A36; then reconsider x = g'.i as Element of R; take R,x,x; x <= x; hence thesis by A8; end; then A37: g' <= g' by A35,YELLOW_1:def 4; I(i,g) c= I(p) proof let u be set; 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 j' = j as Element of X; reconsider q = [j,g] as Element of Iterated J by A11,A31,ZFMISC_1:106; [j',g'] >= [i',g'] by A37,A39,YELLOW_3:11; then A40: q >= p by A33,A34,Lm1; u = (the mapping of Iterated J). [j,g] by A38,BINOP_1:def 1 .= (Iterated J).q by WAYBEL_0:def 8; hence u in I(p) by A40; end; then A41: "/\"(I(p),L) <= "/\"(I(i,g),L) by WAYBEL_7:3; 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 SubsetFD; 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 SubsetFD; 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:9; reconsider k' = 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; f in product Carrier J; then f in the carrier of product J by YELLOW_1:def 4; then reconsider f' = f as Element of product J; A45: [k',f'] >= [i',g'] by A33,A34,A43,A44,Lm1; then i <= k by YELLOW_3:11; hence a in A; reconsider k' = k as Element of I; set N = Net-Str(K.k',F.k'); A46: J.k = N by A8; reconsider g'k =g'.k, f'k = f'.k as Element of N by A8; A47: b = (the mapping of J.k).(f'.k) by A42,A44,YELLOW_6:36 .= N.(f'k) by A46,WAYBEL_0:def 8; reconsider kg = [k,g] as Element of Iterated J by A11,A31,ZFMISC_1:106; A48: a = (the mapping of Iterated J).kg by BINOP_1:def 1 .= (Iterated J).kg by WAYBEL_0:def 8 .= (the mapping of J.k).(g'.k) by YELLOW_6:36 .= N.(g'k) by A46,WAYBEL_0:def 8; g' <= f' by A45,YELLOW_3:11; then g'.k <= f'.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 "/\"(I(p),L) = "/\"(I(i,g),L) by A41,YELLOW_0:def 3; end; thus D c= D' proof let e be set; 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:9; e = "/\"(I(j,g),L) by A32,A49,A50; hence e in D'; end; let e be set; assume e in D'; 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,A31,ZFMISC_1:106; e = "/\"(I(j),L) by A32,A51; hence e in D; end; A52: E' = D' from Irrel(A22); :: UWAGA!!! wrazliwy na strony rownosci for y being set holds y in E' iff ex x being set st x in dom(Infs Frege F) & y = (Infs Frege F).x proof let y be set; thus y in E' implies ex x being set st x in dom(Infs Frege F) & y = (Infs Frege F).x proof assume y in E'; then consider g being Element of product doms F such that A53: y = "/\"(rng((Frege F).g),L); take g; thus g in dom(Infs Frege F) by A13; then A54: g in dom(Frege F) by FUNCT_2:def 1; 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 set 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 A12,A55,FUNCT_2:def 1; x in dom(Frege F) by A55,FUNCT_2:def 1; then y = //\((Frege F).x, L) by A56,WAYBEL_5:def 2 .= "/\"(rng((Frege F).x),L) by YELLOW_2:def 6; hence y in E'; end; then rng Infs Frege F = E' by FUNCT_1:def 5; then A57: Sup Infs Frege F = "\/"(D,L) by A30,A52,YELLOW_2:def 5 .= lim_inf Iterated J by Def6; reconsider x' = x as Element of L; set X1 = {x where j' is Element of X: not contradiction}, X2 = {"/\"({X.i where i is Element of X:i >= j},L) where j is Element of X: not contradiction}; 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 set holds e in X3 iff ex u being set st u in dom Sups F & e = (Sups F).u proof let e be set; 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 set; take u; u in I; hence u in dom Sups F by FUNCT_2:def 1; thus e = (Sups F).u by A60,WAYBEL_0:def 8; end; given u being set 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,WAYBEL_0:def 8; hence e in X3 by A63; end; then rng Sups F = X3 by FUNCT_1:def 5; hence x = "/\"(X3,L) by YELLOW_2:def 6; end; thus X2 c= X1 proof let u be set; assume u in X2; then consider j being Element of X such that A64: u = "/\"({X.i where i is Element of X:i >= j},L); u = x by A59,A64; hence u in X1; end; let u be set; consider j being 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 u in X2; end; now let u be set; u in X1 iff ex j' 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 {x'} by A58,TARSKI:2 .= x by YELLOW_0:39; then x <= lim_inf X by Def6; then x is_S-limit_of X by Def7; then [X,x] in C by A20,Def8; then [Iterated J,x] in C by A1,A16,YELLOW_6:def 26; then x is_S-limit_of Iterated J by A21,Def8; then x <= Sup Infs Frege F by A57,Def7; hence x = Sup Infs Frege F by A5,ORDERS_1:25; end; hence L is continuous 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:53; 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,WAYBEL_3:def 1; d in S by A2,A5,WAYBEL_0:def 20; hence D meets S by A4,XBOOLE_0:3; end; hence S is open 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 set; assume A2: e in uparrow x; then reconsider y = e as Element of L; x <= y by A2,WAYBEL_0:18; hence e in S 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,Def1; then (waybelow p) /\ S <> {} by XBOOLE_0:def 7; then consider u being Element of L such that A4: u in (waybelow p) /\ S by SUBSET_1:10; reconsider u as Element of L; take u; u in waybelow p by A4,XBOOLE_0:def 3; hence u << p by WAYBEL_3:7; thus u in S by A4,XBOOLE_0:def 3; 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 set; assume e in X; then ex q being Element of L st e = wayabove q & q << p; hence e in bool the carrier of L; end; then X is Subset-Family of L by SETFAM_1:def 7; then reconsider X as Subset-Family of L; X is Basis of p proof thus X c= the topology of L proof let e be set; assume e in X; then consider q being Element of L such that A1: e = wayabove q and q << p; wayabove q is open by Th36; hence e in the topology of L by A1,PRE_TOPC:def 5; end; 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 p in e by WAYBEL_3:8; end; hence p in Intersect X by CANTOR_1:10; let S be Subset of L such that A2: S is open and A3: p in S; consider u being Element of L such that A4: u << p and A5: u in S by A2,A3,Th43; take V = wayabove u; thus V in X by A4; A6: S is upper by A2,Def4; A7: wayabove u c= uparrow u by WAYBEL_3:11; uparrow u c= S by A5,A6,Th42; hence V c= S by A7,XBOOLE_1:1; end; hence thesis; end; theorem Th45: for T being complete continuous Scott TopLattice holds { wayabove x where x is Element of T: not contradiction } is Basis of T proof let T be complete continuous Scott TopLattice; set B = { wayabove x where x is Element of T: not contradiction }; A1: B c= the topology of T proof let e be set; assume e in B; then consider x being Element of T such that A2: e = wayabove x; wayabove x is open by Th36; hence e in the topology of T by A2,PRE_TOPC:def 5; end; then B c= bool the carrier of T by XBOOLE_1:1; then B is Subset-Family of T by SETFAM_1:def 7; then reconsider P = B as Subset-Family of T; 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 set; assume u in A; then ex q being Element of T st u = wayabove q & q << p; hence u in P; end; hence B is Basis of T by A1,YELLOW_8:23; 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 set; assume A1: y in Int uparrow p; then reconsider q = y as Element of T; reconsider S = Int uparrow p as Subset of T; S is open by TOPS_1:51; then 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:44; then p <= u by A3,WAYBEL_0:18; then p << q by A2,WAYBEL_3:2; hence y in wayabove p by WAYBEL_3:8; end; A4: wayabove p is open by Th36; wayabove p c= uparrow p by WAYBEL_3:11; hence wayabove p c= Int uparrow p by A4,TOPS_1:56; 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 = { wayabove x where x is Element of T: not contradiction }, 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 set; 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 e in P by A2,A4; end; let e be set; 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 e in I by A5,A6; end; B is Basis of T by Th45; hence Int S = union P by A1,YELLOW_8:20; end;

Back to top