:: Scott Topology :: by Andrzej Trybulec :: :: Received January 29, 1997 :: Copyright (c) 1997-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, TARSKI, REWRITE1, WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, EQREL_1, RELAT_2, FINSET_1, ORDINAL2, YELLOW_0, ZFMISC_1, STRUCT_0, CARD_1, RELAT_1, CARD_FIL, WAYBEL_9, RCOMP_1, NATTRA_1, PRE_TOPC, T_0TOPSP, CONNSP_2, TOPS_1, FUNCT_1, YELLOW_6, SEQM_3, CLASSES2, CLASSES1, YELLOW_2, PROB_1, WAYBEL_3, ORDINAL1, CARD_3, PBOOLE, WAYBEL_5, FUNCT_6, RLVECT_2, WAYBEL_6, RLVECT_3, YELLOW_8, WAYBEL11; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, DOMAIN_1, ORDINAL1, NUMBERS, STRUCT_0, WAYBEL_6, PRE_TOPC, TOPS_1, TOPS_2, CANTOR_1, CONNSP_2, T_0TOPSP, TDLAT_3, PBOOLE, CLASSES1, CLASSES2, CARD_3, PRALG_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_6, WAYBEL_9, YELLOW_8; constructors DOMAIN_1, CLASSES1, CLASSES2, TOPS_1, CONNSP_2, TDLAT_3, T_0TOPSP, CANTOR_1, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_9, YELLOW_8, RELSET_1, TOPS_2, WAYBEL_2, NUMBERS; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, TDLAT_3, WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_5, WAYBEL_9, RELSET_1, TOPS_1; requirements SUBSET, BOOLE, NUMERALS; begin scheme :: WAYBEL11:sch 1 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 for i being Element of I(), u being Element of D() holds F(u) = F(i,u); theorem :: WAYBEL11:1 for L being complete LATTICE, X,Y being Subset of L st Y is_coarser_than X holds "/\"(X,L) <= "/\"(Y,L); theorem :: WAYBEL11:2 for L being complete LATTICE, X,Y being Subset of L st X is_finer_than Y holds "\/"(X,L) <= "\/"(Y,L); theorem :: WAYBEL11:3 for T being RelStr, A being upper Subset of T, B being directed Subset of T holds A /\ B is directed; registration let T be reflexive non empty RelStr; cluster non empty directed finite for Subset of T; end; theorem :: WAYBEL11:4 :: uogolnione WAYBEL_3:16 for T being with_suprema Poset, D being non empty directed finite Subset of T holds sup D in D; registration cluster reflexive transitive 1-element antisymmetric with_suprema with_infima finite strict for RelStr; end; registration let T be finite 1-sorted; cluster -> finite for Subset of T; end; registration let R be RelStr; cluster empty -> lower upper for Subset of R; end; registration let R be 1-element RelStr; cluster -> upper for Subset of R; end; theorem :: WAYBEL11:5 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; theorem :: WAYBEL11:6 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; begin :: Scott Topology definition let T be non empty reflexive RelStr, S be Subset of T; attr S is inaccessible_by_directed_joins means :: WAYBEL11:def 1 for D being non empty directed Subset of T st sup D in S holds D meets S; attr S is closed_under_directed_sups means :: WAYBEL11:def 2 for D being non empty directed Subset of T st D c= S holds sup D in S; attr S is property(S) means :: WAYBEL11:def 3 for D being non empty directed Subset of T st sup D in S ex y being Element of T st y in D & for x being Element of T st x in D & x >= y holds x in S; end; notation let T be non empty reflexive RelStr, S be Subset of T; synonym S is inaccessible for S is inaccessible_by_directed_joins; synonym S is directly_closed for S is closed_under_directed_sups; end; registration let T be non empty reflexive RelStr; cluster empty -> property(S) directly_closed for Subset of T; end; registration let T be non empty reflexive RelStr; cluster property(S) directly_closed for Subset of T; end; registration let T be non empty reflexive RelStr, S be property(S) Subset of T; cluster S` -> directly_closed; end; definition let T be reflexive non empty TopRelStr; attr T is Scott means :: WAYBEL11:def 4 for S being Subset of T holds S is open iff S is inaccessible upper; end; registration let T be reflexive transitive antisymmetric non empty with_suprema finite RelStr; cluster -> inaccessible for Subset of T; end; definition let T be reflexive transitive antisymmetric non empty with_suprema finite TopRelStr; redefine attr T is Scott means :: WAYBEL11:def 5 for S being Subset of T holds S is open iff S is upper; end; registration cluster complete strict 1-element Scott for TopLattice; end; registration let T be non empty reflexive RelStr; cluster [#]T -> directly_closed inaccessible; end; registration let T be non empty reflexive RelStr; cluster directly_closed lower inaccessible upper for Subset of T; end; registration let T be non empty reflexive RelStr, S be inaccessible Subset of T; cluster S` -> directly_closed; end; registration let T be non empty reflexive RelStr, S be directly_closed Subset of T; cluster S` -> inaccessible; end; theorem :: WAYBEL11:7 :: 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; theorem :: WAYBEL11:8 for T being up-complete non empty reflexive transitive antisymmetric TopRelStr, x being Element of T holds downarrow x is directly_closed; theorem :: WAYBEL11:9 :: p. 100, Remark 1.4 (ii) for T being complete Scott TopLattice, x being Element of T holds Cl {x} = downarrow x; theorem :: WAYBEL11:10 :: p. 100, Remark 1.4 (iii) for T being complete Scott TopLattice holds T is T_0-TopSpace; theorem :: WAYBEL11:11 for T being Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, x being Element of T holds downarrow x is closed; theorem :: WAYBEL11:12 for T being up-complete Scott TopLattice, x being Element of T holds (downarrow x)` is open; theorem :: WAYBEL11:13 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; theorem :: WAYBEL11:14 :: 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; theorem :: WAYBEL11:15 :: 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); registration let T be complete TopLattice; :: p. 100, Remark 1.4 (vi) cluster lower -> property(S) for Subset of T; end; theorem :: WAYBEL11:16 :: p. 100, Remark 1.4 (vii) for T being non empty transitive reflexive TopRelStr st the topology of T = { S where S is Subset of T: S is property(S)} holds T is TopSpace-like; 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 :: WAYBEL11:def 6 "\/"((the set of all "/\"({N.i:i >= j},R) where j is Element of N),R); 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 :: WAYBEL11:def 7 p <= lim_inf N; end; definition let R be reflexive non empty RelStr; func Scott-Convergence R -> Convergence-Class of R means :: WAYBEL11:def 8 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; end; :: remarks, p.98 theorem :: WAYBEL11:17 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; theorem :: WAYBEL11:18 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; definition let R be reflexive non empty RelStr, N be non empty NetStr over R; redefine attr N is monotone means :: WAYBEL11:def 9 for i,j being Element of N st i <= j holds N.i <= N.j; 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 :: WAYBEL11:def 10 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; end; theorem :: WAYBEL11:19 for L being non empty 1-sorted, N being non empty NetStr over L holds rng the mapping of N = the set of all N.i where i is Element of N; theorem :: WAYBEL11:20 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; registration let R be non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; cluster Net-Str(S,f) -> monotone; end; registration let R be transitive non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; cluster Net-Str(S,f) -> transitive; end; registration let R be reflexive non empty RelStr; let S be non empty set, f be Function of S, the carrier of R; cluster Net-Str(S,f) -> reflexive; end; theorem :: WAYBEL11:21 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; registration let R be LATTICE; cluster monotone reflexive strict for net of R; end; theorem :: WAYBEL11:22 for R being complete LATTICE, N being monotone reflexive net of R holds lim_inf N = sup N; theorem :: WAYBEL11:23 for R being complete LATTICE, N being constant net of R holds the_value_of N = lim_inf N; theorem :: WAYBEL11:24 for R being complete LATTICE, N being constant net of R holds the_value_of N is_S-limit_of N; definition let S be non empty 1-sorted, e be Element of S; func Net-Str e -> strict NetStr over S means :: WAYBEL11:def 11 the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e}; end; registration let S be non empty 1-sorted, e be Element of S; cluster Net-Str e -> non empty; end; theorem :: WAYBEL11:25 for S being non empty 1-sorted, e being Element of S, x being Element of Net-Str e holds x = e; theorem :: WAYBEL11:26 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; registration let S be non empty 1-sorted, e be Element of S; cluster Net-Str e -> reflexive transitive directed antisymmetric; end; theorem :: WAYBEL11:27 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; theorem :: WAYBEL11:28 for S being reflexive antisymmetric non empty RelStr, e being Element of S holds e = lim_inf Net-Str e; theorem :: WAYBEL11:29 for S being non empty reflexive RelStr, e being Element of S holds Net-Str e in NetUniv S; theorem :: WAYBEL11:30 for R being complete LATTICE, Z be net of R, D be Subset of R st D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R) where j is Element of Z holds D is non empty directed; theorem :: WAYBEL11:31 :: 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; theorem :: WAYBEL11:32 for T being complete Scott TopLattice holds the TopStruct of T = ConvergenceSpace Scott-Convergence T; theorem :: WAYBEL11:33 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; theorem :: WAYBEL11:34 for T being complete TopLattice st the TopStruct of T = ConvergenceSpace Scott-Convergence T holds T is Scott; registration let R be complete LATTICE; :: 1.6. Proposition (i) cluster Scott-Convergence R -> (CONSTANTS); end; registration let R be complete LATTICE; :: 1.6. Proposition (i) cluster Scott-Convergence R -> (SUBNETS); end; theorem :: WAYBEL11:35 :: 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; definition let L be non empty reflexive RelStr; func sigma L -> Subset-Family of L equals :: WAYBEL11:def 12 the topology of ConvergenceSpace Scott-Convergence L; end; theorem :: WAYBEL11:36 :: 1.5 Examples (5), p.100 for L being continuous complete Scott TopLattice, x be Element of L holds wayabove x is open; theorem :: WAYBEL11:37 for T being complete TopLattice st the topology of T = sigma T holds T is Scott; registration let R be continuous complete LATTICE; :: 1.6. Proposition (ii) cluster Scott-Convergence R -> topological; end; theorem :: WAYBEL11:38 :: 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; theorem :: WAYBEL11:39 :: 1.7. Lemma for L being complete non empty Poset st Scott-Convergence L is (ITERATED_LIMITS) holds L is continuous; theorem :: WAYBEL11:40 :: 1.8 Theorem, p.104 for T being complete Scott TopLattice holds T is continuous iff Convergence T = Scott-Convergence T; theorem :: WAYBEL11:41 :: 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; theorem :: WAYBEL11:42 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; theorem :: WAYBEL11:43 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; theorem :: WAYBEL11:44 :: 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; theorem :: WAYBEL11:45 for T being complete continuous Scott TopLattice holds the set of all wayabove x where x is Element of T is Basis of T; theorem :: WAYBEL11:46 :: 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; theorem :: WAYBEL11:47 :: 1.10. Propostion (iii), p.104 for T being complete continuous Scott TopLattice, p being Element of T holds Int uparrow p = wayabove p; theorem :: WAYBEL11:48 :: 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};