Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Moore-Smith Convergence

**by****Andrzej Trybulec**- Received November 12, 1996
- MML identifier: YELLOW_6

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCOP_1, SEQM_3, RELAT_1, FUNCT_1, BOOLE, CARD_1, ZF_LANG, ORDINAL1, CLASSES1, CLASSES2, CARD_3, FUNCT_2, PROB_1, TARSKI, PRE_TOPC, CONNSP_2, TOPS_1, COMPTS_1, COMPLSP1, SUBSET_1, PRALG_1, PBOOLE, RLVECT_2, WAYBEL_3, YELLOW_1, FRAENKEL, ZF_REFLE, ORDERS_1, WAYBEL_0, QUANTAL1, LATTICES, RELAT_2, CAT_1, YELLOW_0, WELLORD1, ORDINAL2, MCART_1, REALSET1, SEQ_2, SETFAM_1, CLOSURE1, YELLOW_6; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, COMPLSP1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, BINOP_1, REALSET1, CARD_1, CARD_3, MSUALG_1, PRE_CIRC, PROB_1, ORDINAL1, CLASSES1, CLASSES2, TOLER_1, SEQM_3, STRUCT_0, TOPS_1, COMPTS_1, CONNSP_2, PBOOLE, PRALG_1, ORDERS_1, LATTICE3, PRE_TOPC, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, FRAENKEL, WAYBEL_3, GRCAT_1; constructors SEQM_3, CLASSES1, TOPS_1, CONNSP_2, COMPTS_1, COMPLSP1, PRALG_1, WAYBEL_3, TOLER_1, YELLOW_3, BINOP_1, MSUALG_1, DOMAIN_1, PRE_CIRC, GRCAT_1, LATTICE3, PROB_1, TOPS_2, PRE_TOPC; clusters SUBSET_1, STRUCT_0, RELSET_1, WAYBEL_0, ORDERS_1, PRALG_1, AMI_1, YELLOW_1, YELLOW_3, INDEX_1, PRE_TOPC, MSUALG_1, COMPLSP1, LATTICE3, YELLOW_0, PBOOLE, FUNCOP_1, RELAT_1, FUNCT_1, CLASSES2, CARD_1, FRAENKEL, SEQM_3, ZFMISC_1; requirements NUMERALS, BOOLE, SUBSET; begin :: Preliminaries, classical mathematics scheme SubsetEq{X()-> non empty set, A,B()-> Subset of X(), P[set]}: A() = B() provided for y being Element of X() holds y in A() iff P[y] and for y being Element of X() holds y in B() iff P[y]; canceled; definition let f be Function; assume f is non empty constant; func the_value_of f means :: YELLOW_6:def 1 ex x being set st x in dom f & it = f.x; end; definition cluster non empty constant Function; end; theorem :: YELLOW_6:2 for X being non empty set, x being set holds the_value_of (X --> x) = x; theorem :: YELLOW_6:3 for f being Function holds Card rng f c= Card dom f; definition cluster universal -> epsilon-transitive being_Tarski-Class set; cluster epsilon-transitive being_Tarski-Class -> universal set; end; reserve x,y,z,X for set, T for Universe; definition let X; canceled; func the_universe_of X equals :: YELLOW_6:def 3 Tarski-Class the_transitive-closure_of X; end; definition let X; cluster the_universe_of X -> epsilon-transitive being_Tarski-Class; end; definition let X; cluster the_universe_of X -> universal non empty; end; canceled; theorem :: YELLOW_6:5 for f being Function st dom f in T & rng f c= T holds product f in T; begin :: Topological spaces, preliminaries theorem :: YELLOW_6:6 :: PRE_TOPC:def 13 for T being non empty TopSpace, A being Subset of T for p being Point of T holds p in Cl A iff for G being a_neighborhood of p holds G meets A; definition let T be non empty TopSpace; redefine attr T is being_T2; synonym T is Hausdorff; end; definition cluster Hausdorff (non empty TopSpace); end; theorem :: YELLOW_6:7 for X be non empty TopSpace, A be Subset of X holds [#]X is a_neighborhood of A; theorem :: YELLOW_6:8 for X be non empty TopSpace, A be Subset of X, Y being a_neighborhood of A holds A c= Y; begin :: 1-sorted structures theorem :: YELLOW_6:9 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; definition cluster non empty constant 1-sorted-yielding Function; end; definition let J be 1-sorted-yielding Function; redefine attr J is non-Empty means :: YELLOW_6:def 4 for i being set st i in rng J holds i is non empty 1-sorted; synonym J is yielding_non-empty_carriers; end; definition let X be set; let L be 1-sorted; cluster X --> L -> 1-sorted-yielding; end; definition let I be set; cluster yielding_non-empty_carriers (1-sorted-yielding ManySortedSet of I); end; definition let I be non empty set; let J be RelStr-yielding ManySortedSet of I; cluster the carrier of product J -> functional; end; definition let I be set; let J be yielding_non-empty_carriers (1-sorted-yielding ManySortedSet of I); cluster Carrier J -> non-empty; end; theorem :: YELLOW_6:10 for T being non empty 1-sorted, S being Subset of T, p being Element of T holds not p in S iff p in S`; begin :: Preliminaries to Relational Structures definition let T be non empty RelStr, A be lower Subset of T; cluster A` -> upper; end; definition 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 5 for x,y being Element of N ex z being Element of N st x <= z & y <= z; end; definition let X be set; cluster BoolePoset X -> directed; end; definition cluster non empty directed transitive strict RelStr; end; definition let M be non empty set, N be non empty RelStr, f be Function of M, the carrier of N, m be Element of M; redefine func f.m -> Element of N; end; definition let I be set; cluster yielding_non-empty_carriers (RelStr-yielding ManySortedSet of I); end; definition let I be non empty set; let J be yielding_non-empty_carriers (RelStr-yielding ManySortedSet of I); cluster product J -> non empty; end; theorem :: YELLOW_6:11 for R1,R2 being RelStr holds [#][:R1,R2:] = [:[#]R1,[#]R2:]; definition let Y1,Y2 be directed RelStr; cluster [:Y1,Y2:] -> directed; end; theorem :: YELLOW_6:12 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 6 the mapping of N is constant; end; definition let R be RelStr, T be non empty 1-sorted, p be Element of T; func R --> p -> strict NetStr over T means :: YELLOW_6:def 7 the RelStr of it = the RelStr of R & the mapping of it = (the carrier of it) --> p; end; definition let R be RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> constant; end; definition let R be non empty RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> non empty; end; definition let R be non empty directed RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> directed; end; definition let R be non empty transitive RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> transitive; end; theorem :: YELLOW_6:13 for R be RelStr, T be non empty 1-sorted, p be Element of T holds the carrier of R --> p = the carrier of R; theorem :: YELLOW_6:14 for R be non empty RelStr, T be non empty 1-sorted, p be Element of T, q be Element of (R-->p) holds (R --> p).q = p; definition 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:15 for R being RelStr holds R is full SubRelStr of R; theorem :: YELLOW_6:16 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 8 it is SubRelStr of N & the mapping of it = (the mapping of N)|the carrier of it; end; theorem :: YELLOW_6:17 for S being 1-sorted, N being NetStr over S holds N is SubNetStr of N; theorem :: YELLOW_6:18 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 9 M is full SubRelStr of N; end; definition let S be 1-sorted, N be NetStr over S; cluster full strict SubNetStr of N; end; definition let S be 1-sorted, N be non empty NetStr over S; cluster full non empty strict SubNetStr of N; end; theorem :: YELLOW_6:19 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:20 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:21 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 definition let T be non empty 1-sorted; cluster constant strict net of T; end; definition 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 10 the_value_of the mapping of N; end; theorem :: YELLOW_6:22 for R be non empty RelStr, T be non empty 1-sorted, p be Element of T holds the_value_of (R --> p) = p; definition let T be non empty 1-sorted, N be net of T; canceled; mode subnet of N -> net of T means :: YELLOW_6:def 12 ex f being map 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:23 for T being non empty 1-sorted, N be net of T holds N is subnet of N; theorem :: YELLOW_6:24 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:25 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:26 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:27 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:28 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:29 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 13 it is full SubRelStr of N & the carrier of it = (the mapping of N)"X; end; definition let S be 1-sorted, N be transitive NetStr over S, X; cluster N"X -> transitive full; end; theorem :: YELLOW_6:30 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:31 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:32 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 means :: YELLOW_6:def 14 for x 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; definition 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 15 for i being set st i in rng it holds i is net of T; end; theorem :: YELLOW_6:33 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; definition let X be set, T be 1-sorted; cluster -> RelStr-yielding net_set of X,T; end; definition let T be 1-sorted, Y be net of T; cluster -> yielding_non-empty_carriers net_set of the carrier of Y,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; cluster product J -> directed transitive; end; definition let X be set, T be 1-sorted; cluster -> yielding_non-empty_carriers net_set of X,T; end; definition let X be set, T be 1-sorted; cluster yielding_non-empty_carriers 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 16 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:34 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:35 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:36 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:37 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 { rng the mapping of J.i where i is Element of Y: not contradiction }; 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 17 (InclPoset { V where V is Subset of T: p in V & V is open })~; end; definition let T be non empty TopSpace, p be Point of T; cluster OpenNeighborhoods p -> non empty; end; theorem :: YELLOW_6:38 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:39 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:40 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; definition 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 18 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:41 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:42 for T being non empty TopSpace, N be constant net of T holds the_value_of N in Lim N; theorem :: YELLOW_6:43 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:44 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; definition 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 19 Lim N <> {}; end; definition let T be non empty TopSpace; cluster constant -> convergent net of T; end; definition let T be non empty TopSpace; cluster convergent strict 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 20 it in Lim N; end; theorem :: YELLOW_6:45 for T be Hausdorff (non empty TopSpace), N be constant net of T holds lim N = the_value_of N; theorem :: YELLOW_6:46 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:47 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:48 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 means :: YELLOW_6:def 21 it c= [:NetUniv S,the carrier of S:]; end; definition let S be non empty 1-sorted; cluster -> Relation-like Convergence-Class of S; end; definition let T be non empty TopSpace; func Convergence T -> Convergence-Class of T means :: YELLOW_6:def 22 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 23 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 24 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 25 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 26 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; definition 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 27 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; definition let S be non empty 1-sorted, C be Convergence-Class of S; cluster ConvergenceSpace C -> non empty; end; definition let S be non empty 1-sorted, C be Convergence-Class of S; cluster ConvergenceSpace C -> TopSpace-like; end; theorem :: YELLOW_6:49 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 28 C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS); end; definition let T be non empty 1-sorted; cluster non empty topological Convergence-Class of T; end; definition let T be non empty 1-sorted; cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) Convergence-Class of T; cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological Convergence-Class of T; end; theorem :: YELLOW_6:50 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:51 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:52 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:53 for T be non empty 1-sorted, C be Convergence-Class of T holds Convergence ConvergenceSpace C = C iff C is topological;

Back to top