:: Moore-Smith Convergence :: by Andrzej Trybulec :: :: Received November 12, 1996 :: Copyright (c) 1996-2021 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 CLASSES2, CLASSES1, ORDINAL1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, CARD_3, CARD_1, FUNCT_2, PRALG_1, PBOOLE, SUBSET_1, RLVECT_2, STRUCT_0, FUNCOP_1, WAYBEL_3, YELLOW_1, ORDERS_2, WAYBEL_0, XXREAL_0, RELAT_2, ZFMISC_1, CAT_1, YELLOW_0, WELLORD1, PRE_TOPC, RCOMP_1, CONNSP_2, COMPTS_1, MCART_1, TOPS_1, SEQ_2, ORDINAL2, SETFAM_1, YELLOW_6; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_1, CARD_3, FUNCOP_1, ORDINAL1, CLASSES1, CLASSES2, TOLER_1, STRUCT_0, TOPS_1, COMPTS_1, CONNSP_2, PRALG_1, ORDERS_2, LATTICE3, PRE_TOPC, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3; constructors BINOP_1, CLASSES1, TOLER_1, CLASSES2, REALSET1, TOPS_1, COMPTS_1, CONNSP_2, LATTICE3, PRALG_1, YELLOW_3, WAYBEL_3, RELSET_1, PBOOLE, XTUPLE_0, WAYBEL_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, CARD_1, CLASSES1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2, PCOMPS_1, LATTICE3, YELLOW_0, WAYBEL_0, PARTFUN1, YELLOW_1, YELLOW_3, WAYBEL_3, RELSET_1, TOPS_1, RELAT_1, XTUPLE_0; requirements BOOLE, SUBSET; begin :: Preliminaries, classical mathematics reserve x,y,z,X for set, T for Universe; definition let X; func the_universe_of X -> set equals :: YELLOW_6:def 1 Tarski-Class the_transitive-closure_of X; end; registration let X; cluster the_universe_of X -> epsilon-transitive Tarski; end; registration let X; cluster the_universe_of X -> universal non empty; end; theorem :: YELLOW_6:1 for f being Function st dom f in T & rng f c= T holds product f in T; begin begin :: 1-sorted structures theorem :: YELLOW_6:2 for Y be non empty set for J being 1-sorted-yielding ManySortedSet of Y, i being Element of Y holds (Carrier J).i = the carrier of J .i; registration cluster non empty constant 1-sorted-yielding for Function; end; notation let J be 1-sorted-yielding Function; synonym J is yielding_non-empty_carriers for J is non-Empty; end; definition let J be 1-sorted-yielding Function; redefine attr J is yielding_non-empty_carriers means :: YELLOW_6:def 2 for i being set st i in rng J holds i is non empty 1-sorted; end; registration let X be set; let L be 1-sorted; cluster X --> L -> 1-sorted-yielding; end; registration let I be set; cluster yielding_non-empty_carriers for 1-sorted-yielding ManySortedSet of I; end; registration let I be non empty set; let J be RelStr-yielding ManySortedSet of I; cluster the carrier of product J -> functional; end; registration let I be set; let J be yielding_non-empty_carriers 1-sorted-yielding ManySortedSet of I; cluster Carrier J -> non-empty; end; begin :: Preliminaries to Relational Structures registration let T be non empty RelStr, A be lower Subset of T; cluster A` -> upper; end; registration let T be non empty RelStr, A be upper Subset of T; cluster A` -> lower; end; definition let N be non empty RelStr; redefine attr N is directed means :: YELLOW_6:def 3 for x,y being Element of N ex z being Element of N st x <= z & y <= z; end; registration let X be set; cluster BoolePoset X -> directed; end; registration cluster non empty directed transitive strict for RelStr; end; registration let I be set; cluster yielding_non-empty_carriers for RelStr-yielding ManySortedSet of I; end; registration let I be non empty set; let J be yielding_non-empty_carriers RelStr-yielding ManySortedSet of I; cluster product J -> non empty; end; registration let Y1,Y2 be directed RelStr; cluster [:Y1,Y2:] -> directed; end; theorem :: YELLOW_6:3 for R being RelStr holds the carrier of R = the carrier of R~; definition let S be 1-sorted, N be NetStr over S; attr N is constant means :: YELLOW_6:def 4 the mapping of N is constant; end; definition let R be RelStr, T be non empty 1-sorted, p be Element of T; func ConstantNet(R,p) -> strict NetStr over T means :: YELLOW_6:def 5 the RelStr of it = the RelStr of R & the mapping of it = (the carrier of it) --> p; end; registration let R be RelStr, T be non empty 1-sorted, p be Element of T; cluster ConstantNet(R,p) -> constant; end; registration let R be non empty RelStr, T be non empty 1-sorted, p be Element of T; cluster ConstantNet(R,p) -> non empty; end; registration let R be non empty directed RelStr, T be non empty 1-sorted, p be Element of T; cluster ConstantNet(R,p) -> directed; end; registration let R be non empty transitive RelStr, T be non empty 1-sorted, p be Element of T; cluster ConstantNet(R,p) -> transitive; end; theorem :: YELLOW_6:4 for R be RelStr, T be non empty 1-sorted, p be Element of T holds the carrier of ConstantNet(R,p) = the carrier of R; theorem :: YELLOW_6:5 for R be non empty RelStr, T be non empty 1-sorted, p be Element of T, q be Element of ConstantNet(R,p) holds ConstantNet(R,p).q = p; registration let T be non empty 1-sorted, N be non empty NetStr over T; cluster the mapping of N -> non empty; end; begin :: Substructures of Nets theorem :: YELLOW_6:6 for R being RelStr holds R is full SubRelStr of R; theorem :: YELLOW_6:7 for R being RelStr, S being SubRelStr of R, T being SubRelStr of S holds T is SubRelStr of R; definition let S be 1-sorted, N be NetStr over S; mode SubNetStr of N -> NetStr over S means :: YELLOW_6:def 6 it is SubRelStr of N & the mapping of it = (the mapping of N)|the carrier of it; end; theorem :: YELLOW_6:8 for S being 1-sorted, N being NetStr over S holds N is SubNetStr of N; theorem :: YELLOW_6:9 for Q being 1-sorted, R being NetStr over Q, S being SubNetStr of R, T being SubNetStr of S holds T is SubNetStr of R; definition let S be 1-sorted, N be NetStr over S, M be SubNetStr of N; attr M is full means :: YELLOW_6:def 7 M is full SubRelStr of N; end; registration let S be 1-sorted, N be NetStr over S; cluster full strict for SubNetStr of N; end; registration let S be 1-sorted, N be non empty NetStr over S; cluster full non empty strict for SubNetStr of N; end; theorem :: YELLOW_6:10 for S being 1-sorted, N being NetStr over S, M be SubNetStr of N holds the carrier of M c= the carrier of N; theorem :: YELLOW_6:11 for S being 1-sorted, N being NetStr over S, M be SubNetStr of N , x,y being Element of N, i,j being Element of M st x = i & y = j & i <= j holds x <= y; theorem :: YELLOW_6:12 for S being 1-sorted, N being non empty NetStr over S, M be non empty full SubNetStr of N, x,y being Element of N, i,j being Element of M st x = i & y = j & x <= y holds i <= j; begin :: More about Nets registration let T be non empty 1-sorted; cluster constant strict for net of T; end; registration let T be non empty 1-sorted, N be constant NetStr over T; cluster the mapping of N -> constant; end; definition let T be non empty 1-sorted, N be NetStr over T; assume N is constant non empty; func the_value_of N -> Element of T equals :: YELLOW_6:def 8 the_value_of the mapping of N; end; theorem :: YELLOW_6:13 for R be non empty RelStr, T be non empty 1-sorted, p be Element of T holds the_value_of (ConstantNet(R,p)) = p; definition let T be non empty 1-sorted, N be net of T; mode subnet of N -> net of T means :: YELLOW_6:def 9 ex f being Function of it, N st the mapping of it = (the mapping of N)*f & for m being Element of N ex n being Element of it st for p being Element of it st n <= p holds m <= f.p; end; theorem :: YELLOW_6:14 for T being non empty 1-sorted, N be net of T holds N is subnet of N; theorem :: YELLOW_6:15 for T being non empty 1-sorted, N1,N2,N3 be net of T st N1 is subnet of N2 & N2 is subnet of N3 holds N1 is subnet of N3; theorem :: YELLOW_6:16 for T being non empty 1-sorted, N be constant net of T, i being Element of N holds N.i = the_value_of N; theorem :: YELLOW_6:17 for L being non empty 1-sorted, N being net of L, X,Y being set st N is_eventually_in X & N is_eventually_in Y holds X meets Y; theorem :: YELLOW_6:18 for S being non empty 1-sorted, N being net of S, M being subnet of N, X st M is_often_in X holds N is_often_in X; theorem :: YELLOW_6:19 for S being non empty 1-sorted, N being net of S, X st N is_eventually_in X holds N is_often_in X; theorem :: YELLOW_6:20 for S being non empty 1-sorted, N being net of S holds N is_eventually_in the carrier of S; begin :: The Restriction of a Net definition let S be 1-sorted, N be NetStr over S, X; func N"X -> strict SubNetStr of N means :: YELLOW_6:def 10 it is full SubRelStr of N & the carrier of it = (the mapping of N)"X; end; registration let S be 1-sorted, N be transitive NetStr over S, X; cluster N"X -> transitive full; end; theorem :: YELLOW_6:21 for S being non empty 1-sorted, N be net of S, X st N is_often_in X holds N"X is non empty directed; theorem :: YELLOW_6:22 for S being non empty 1-sorted, N being net of S, X st N is_often_in X holds N"X is subnet of N; theorem :: YELLOW_6:23 for S being non empty 1-sorted, N being net of S, X for M being subnet of N st M = N"X holds M is_eventually_in X; begin :: The Universe of Nets definition let X be non empty 1-sorted; func NetUniv X -> set means :: YELLOW_6:def 11 for x being object holds x in it iff ex N being strict net of X st N = x & the carrier of N in the_universe_of the carrier of X; end; registration let X be non empty 1-sorted; cluster NetUniv X -> non empty; end; begin :: Parametrized Families of Nets, Iteration definition let X be set, T be 1-sorted; mode net_set of X,T -> ManySortedSet of X means :: YELLOW_6:def 12 for i being set st i in rng it holds i is net of T; end; theorem :: YELLOW_6:24 for X being set, T being 1-sorted, F being ManySortedSet of X holds F is net_set of X,T iff for i being set st i in X holds F.i is net of T ; definition let X be non empty set, T be 1-sorted; let J be net_set of X,T, i be Element of X; redefine func J.i -> net of T; end; registration let X be set, T be 1-sorted; cluster -> RelStr-yielding for net_set of X,T; end; registration let T be 1-sorted, Y be net of T; cluster -> yielding_non-empty_carriers for net_set of the carrier of Y,T; end; registration let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y ,T; cluster product J -> directed transitive; end; registration let X be set, T be 1-sorted; cluster -> yielding_non-empty_carriers for net_set of X,T; end; registration let X be set, T be 1-sorted; cluster yielding_non-empty_carriers for net_set of X,T; end; definition let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y ,T; func Iterated J -> strict net of T means :: YELLOW_6:def 13 the RelStr of it = [:Y, product J:] & for i being Element of Y, f being Function st i in the carrier of Y & f in the carrier of product J holds (the mapping of it).(i,f) =(the mapping of J.i).(f.i); end; theorem :: YELLOW_6:25 for T being non empty 1-sorted, Y being net of T, J being net_set of the carrier of Y,T st Y in NetUniv T & for i being Element of Y holds J.i in NetUniv T holds Iterated J in NetUniv T; theorem :: YELLOW_6:26 for T being non empty 1-sorted, N being net of T for J being net_set of the carrier of N, T holds the carrier of Iterated J = [:the carrier of N, product Carrier J:]; theorem :: YELLOW_6:27 for T being non empty 1-sorted, N being net of T, J being net_set of the carrier of N, T, i being Element of N, f being Element of product J, x being Element of Iterated J st x = [i,f] holds (Iterated J).x = ( the mapping of J.i).(f.i); theorem :: YELLOW_6:28 for T being non empty 1-sorted, Y being net of T, J being net_set of the carrier of Y,T holds rng the mapping of Iterated J c= union the set of all rng the mapping of J.i where i is Element of Y; begin :: Poset of open neighborhoods definition let T be non empty TopSpace, p be Point of T; func OpenNeighborhoods p -> RelStr equals :: YELLOW_6:def 14 (InclPoset { V where V is Subset of T: p in V & V is open })~; end; registration let T be non empty TopSpace, p be Point of T; cluster OpenNeighborhoods p -> non empty; end; theorem :: YELLOW_6:29 for T being non empty TopSpace, p being Point of T, x being Element of OpenNeighborhoods p ex W being Subset of T st W = x & p in W & W is open; theorem :: YELLOW_6:30 for T be non empty TopSpace, p be Point of T for x being Subset of T holds x in the carrier of OpenNeighborhoods p iff p in x & x is open; theorem :: YELLOW_6:31 for T be non empty TopSpace, p be Point of T for x,y being Element of OpenNeighborhoods p holds x <= y iff y c= x; registration let T be non empty TopSpace, p be Point of T; cluster OpenNeighborhoods p -> transitive directed; end; begin :: Nets in topological spaces definition let T be non empty TopSpace, N be net of T; func Lim N -> Subset of T means :: YELLOW_6:def 15 for p being Point of T holds p in it iff for V being a_neighborhood of p holds N is_eventually_in V; end; theorem :: YELLOW_6:32 for T being non empty TopSpace, N being net of T, Y being subnet of N holds Lim N c= Lim Y; theorem :: YELLOW_6:33 for T being non empty TopSpace, N be constant net of T holds the_value_of N in Lim N; theorem :: YELLOW_6:34 for T being non empty TopSpace, N be net of T, p be Point of T st p in Lim N for d being Element of N ex S being Subset of T st S = { N.c where c is Element of N : d <= c } & p in Cl S; theorem :: YELLOW_6:35 for T being non empty TopSpace holds T is Hausdorff iff for N being net of T, p,q being Point of T st p in Lim N & q in Lim N holds p = q; registration let T be Hausdorff non empty TopSpace, N be net of T; cluster Lim N -> trivial; end; definition let T be non empty TopSpace, N be net of T; attr N is convergent means :: YELLOW_6:def 16 Lim N <> {}; end; registration let T be non empty TopSpace; cluster constant -> convergent for net of T; end; registration let T be non empty TopSpace; cluster convergent strict for net of T; end; definition let T be Hausdorff non empty TopSpace, N be convergent net of T; func lim N -> Element of T means :: YELLOW_6:def 17 it in Lim N; end; theorem :: YELLOW_6:36 for T be Hausdorff non empty TopSpace, N be constant net of T holds lim N = the_value_of N; theorem :: YELLOW_6:37 for T being non empty TopSpace, N being net of T for p being Point of T st not p in Lim N ex Y being subnet of N st not ex Z being subnet of Y st p in Lim Z; theorem :: YELLOW_6:38 for T being non empty TopSpace, N being net of T st N in NetUniv T for p being Point of T st not p in Lim N ex Y being subnet of N st Y in NetUniv T & not ex Z being subnet of Y st p in Lim Z; theorem :: YELLOW_6:39 for T being non empty TopSpace, N being net of T, p being Point of T st p in Lim N for J being net_set of the carrier of N, T st for i being Element of N holds N.i in Lim(J.i) holds p in Lim Iterated J; begin :: Convergence Classes definition let S be non empty 1-sorted; mode Convergence-Class of S -> set means :: YELLOW_6:def 18 it c= [:NetUniv S,the carrier of S :]; end; registration let S be non empty 1-sorted; cluster -> Relation-like for Convergence-Class of S; end; definition let T be non empty TopSpace; func Convergence T -> Convergence-Class of T means :: YELLOW_6:def 19 for N being net of T, p being Point of T holds [N,p] in it iff N in NetUniv T & p in Lim N; end; definition let T be non empty 1-sorted, C be Convergence-Class of T; attr C is (CONSTANTS) means :: YELLOW_6:def 20 for N being constant net of T st N in NetUniv T holds [N,the_value_of N] in C; attr C is (SUBNETS) means :: YELLOW_6:def 21 for N being net of T, Y being subnet of N st Y in NetUniv T for p being Element of T holds [N,p] in C implies [Y,p] in C; attr C is (DIVERGENCE) means :: YELLOW_6:def 22 for X being net of T, p being Element of T st X in NetUniv T & not [X,p] in C ex Y being subnet of X st Y in NetUniv T & not ex Z being subnet of Y st [Z,p] in C; attr C is (ITERATED_LIMITS) means :: YELLOW_6:def 23 for X being net of T, p being Element of T st [X,p] in C for J being net_set of the carrier of X, T st for i being Element of X holds [J.i,X.i] in C holds [Iterated J,p] in C; end; registration let T be non empty TopSpace; cluster Convergence T -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS); end; definition let S be non empty 1-sorted, C be Convergence-Class of S; func ConvergenceSpace C -> strict TopStruct means :: YELLOW_6:def 24 the carrier of it = the carrier of S & the topology of it = { V where V is Subset of S: for p being Element of S st p in V for N being net of S st [N,p] in C holds N is_eventually_in V}; end; registration let S be non empty 1-sorted, C be Convergence-Class of S; cluster ConvergenceSpace C -> non empty; end; registration let S be non empty 1-sorted, C be Convergence-Class of S; cluster ConvergenceSpace C -> TopSpace-like; end; theorem :: YELLOW_6:40 for S be non empty 1-sorted, C be Convergence-Class of S holds C c= Convergence ConvergenceSpace C; definition let T be non empty 1-sorted, C be Convergence-Class of T; attr C is topological means :: YELLOW_6:def 25 C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS); end; registration let T be non empty 1-sorted; cluster non empty topological for Convergence-Class of T; end; registration let T be non empty 1-sorted; cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) for Convergence-Class of T; cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological for Convergence-Class of T; end; theorem :: YELLOW_6:41 for T being non empty 1-sorted, C being topological Convergence-Class of T, S being Subset of (ConvergenceSpace C qua non empty TopSpace) holds S is open iff for p being Element of T st p in S for N being net of T st [N,p] in C holds N is_eventually_in S; theorem :: YELLOW_6:42 for T being non empty 1-sorted, C being topological Convergence-Class of T, S being Subset of (ConvergenceSpace C qua non empty TopSpace) holds S is closed iff for p being Element of T holds for N being net of T st [N,p] in C & N is_often_in S holds p in S; theorem :: YELLOW_6:43 for T being non empty 1-sorted, C being topological Convergence-Class of T, S being Subset of ConvergenceSpace C, p being Point of ConvergenceSpace C st p in Cl S ex N being net of ConvergenceSpace C st [N,p] in C & rng the mapping of N c= S & p in Lim N; theorem :: YELLOW_6:44 for T be non empty 1-sorted, C be Convergence-Class of T holds Convergence ConvergenceSpace C = C iff C is topological;