:: Summable Family in a Commutative Group :: by Roland Coghetto :: :: Received August 14, 2015 :: Copyright (c) 2015-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 POLYNOM1, PBOOLE, NAT_1, NUMBERS, FRECHET, PCOMPS_1, REAL_1, CARDFIL2, YELLOW13, CARD_1, XBOOLE_0, SUBSET_1, TARSKI, ORDINAL1, FUNCT_1, PRE_TOPC, STRUCT_0, XXREAL_0, RCOMP_1, METRIC_1, ARYTM_3, YELLOW19, NORMSP_1, NORMSP_2, ARYTM_1, SETFAM_1, ALGSTR_0, ZFMISC_1, SUPINF_2, CONNSP_2, TOPS_1, RELAT_2, RLTOPSP1, FILTER_0, XXREAL_1, ORDERS_2, WAYBEL_0, BINOP_1, RELAT_1, CARD_3, FUNCT_2, FINSUB_1, FINSEQ_1, FINSOP_1, SETWISEO, ORDINAL4, VECTSP_1, SERIES_1, YELLOW_1, TOPGRP_1, GROUP_1, SERIES_3, CARDFIL3, RLVECT_1, GROUP_1A; notations CARDFIL2, GROUP_1A, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, TOPS_1, CONNSP_2, YELLOW13, RUSUB_4, RLTOPSP1, ORDERS_2, WAYBEL_0, METRIC_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, XXREAL_0, STRUCT_0, ALGSTR_0, PRE_TOPC, NORMSP_0, NORMSP_1, NORMSP_2, FRECHET, YELLOW19, PCOMPS_1, ZFMISC_1, BINOP_1, PBOOLE, RELAT_1, FINSUB_1, RLVECT_1, FINSEQ_1, FINSOP_1, SETWISEO, VECTSP_1, YELLOW_1, TOPGRP_1, GROUP_1; constructors YELLOW_8, FRECHET, YELLOW19, TOPS_2, NAT_LAT, NORMSP_2, TOPS_1, RUSUB_4, YELLOW13, FINSOP_1, SETWISEO, FINSEQOP, MEMBERED, NAT_1, BORSUK_1, CARDFIL2, GROUP_1A; registrations GROUP_1A, PCOMPS_1, FRECHET, YELLOW19, XXREAL_0, XREAL_0, NAT_1, SUBSET_1, STRUCT_0, XCMPLX_0, CARD_1, METRIC_1, TOPS_1, RLVECT_1, RLTOPSP1, RELAT_1, XBOOLE_0, FUNCT_1, FINSEQ_1, PBOOLE, FINSUB_1, FVSUM_1, OSALG_1, YELLOW_1, TOPGRP_1, GROUP_1, MEMBERED, ORDERS_2; requirements REAL, NUMERALS, SUBSET, BOOLE; begin :: Preliminaries theorem :: CARDFIL3:1 for I being set holds {} is Element of Fin I; theorem :: CARDFIL3:2 for I,J being set st J in Fin I holds ex p being FinSequence of I st J = rng p & p is one-to-one; theorem :: CARDFIL3:3 for I being set, Y being non empty set, x being Y-valued ManySortedSet of I, p being FinSequence of I holds p*x is FinSequence of Y; theorem :: CARDFIL3:4 for I,X being non empty set, x being X-valued ManySortedSet of I, p,q being FinSequence of I holds (p^q) * x = (p * x) ^ (q * x); definition let I being set, Y being non empty set, x being Y-valued ManySortedSet of I, p being FinSequence of I; func #(p,x) -> FinSequence of Y equals :: CARDFIL3:def 1 p*x; end; definition let I being set; func OrderedFIN I -> non empty transitive reflexive RelStr equals :: CARDFIL3:def 2 InclPoset Fin I; end; theorem :: CARDFIL3:5 for I being set holds [#]OrderedFIN I is directed; begin :: Convergence in TopSpaceMetr theorem :: CARDFIL3:6 for M being non empty MetrSpace, x being Point of TopSpaceMetr(M) holds Balls(x) is basis of BOOL2F NeighborhoodSystem x; theorem :: CARDFIL3:7 for M being non empty MetrSpace, L being non empty transitive reflexive RelStr, f being Function of [#]L,the carrier of TopSpaceMetr(M), x being Point of TopSpaceMetr(M), B being basis of BOOL2F NeighborhoodSystem x st [#]L is directed holds x in lim_f f iff for b being Element of B ex i being Element of L st for j being Element of L st i <=j holds f.j in b; theorem :: CARDFIL3:8 for M being non empty MetrSpace, L being non empty transitive reflexive RelStr, f being Function of [#]L,the carrier of TopSpaceMetr(M), x being Point of TopSpaceMetr(M) st [#]L is directed holds x in lim_f f iff for b being Element of Balls(x) ex n being Element of L st for m being Element of L st n <= m holds f.m in b; theorem :: CARDFIL3:9 for M being non empty MetrSpace, s being sequence of the carrier of TopSpaceMetr(M), x being Point of TopSpaceMetr(M) holds x in lim_f s iff for b being Element of Balls(x) ex i being Nat st for j being Nat st i <=j holds s.j in b; theorem :: CARDFIL3:10 for T being non empty TopStruct, s being sequence of T, x being Point of T holds x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 ex n being Nat st for m being Nat st n <= m holds s.m in U1; theorem :: CARDFIL3:11 for M being non empty MetrSpace, s being sequence of the carrier of TopSpaceMetr(M), x being Point of TopSpaceMetr(M) holds x in Lim s iff for b being Element of Balls(x) ex n being Nat st for m being Nat st n <= m holds s.m in b; theorem :: CARDFIL3:12 for M being non empty MetrSpace, s being sequence of the carrier of TopSpaceMetr(M), x being Point of TopSpaceMetr(M) holds x in lim_f s iff x in Lim s; begin :: Convergence in RealNormSpace theorem :: CARDFIL3:13 for N being RealNormSpace, L being non empty transitive reflexive RelStr, f being Function of [#]L,the carrier of TopSpaceMetr MetricSpaceNorm(N), x being Point of TopSpaceMetr MetricSpaceNorm(N), B being basis of BOOL2F NeighborhoodSystem x st [#]L is directed holds x in lim_f f iff for b being Element of B ex i be Element of L st for j being Element of L st i <=j holds f.j in b; theorem :: CARDFIL3:14 for N being RealNormSpace, x being Point of TopSpaceMetr MetricSpaceNorm N holds Balls(x) is basis of BOOL2F NeighborhoodSystem x; theorem :: CARDFIL3:15 for N being RealNormSpace, s being sequence of the carrier of TopSpaceMetr MetricSpaceNorm(N), x being Point of TopSpaceMetr MetricSpaceNorm N holds x in lim_f s iff for b being Element of Balls(x) ex i being Nat st for j being Nat st i <=j holds s.j in b; theorem :: CARDFIL3:16 for N being RealNormSpace, x being Point of TopSpaceMetr MetricSpaceNorm N holds ex y being Point of MetricSpaceNorm N st y = x & Balls x= {Ball(y,1/n) where n is Nat:n <> 0}; theorem :: CARDFIL3:17 for N being RealNormSpace, x being Point of TopSpaceMetr MetricSpaceNorm N, y being Point of MetricSpaceNorm N, n being positive Nat st x=y holds Ball(y,1/n) in Balls x; theorem :: CARDFIL3:18 for N being RealNormSpace, x being Point of MetricSpaceNorm N, n being Nat st n <> 0 holds Ball (x,1/n) = {q where q is Element of MetricSpaceNorm N : dist(x,q) < 1/n}; theorem :: CARDFIL3:19 for N being RealNormSpace, x being Element of MetricSpaceNorm N, n being Nat st n <> 0 holds ex y being Point of N st x=y & Ball (x,1/n) = {q where q is Point of N : ||.y-q.|| < 1/n}; theorem :: CARDFIL3:20 for PM being MetrStruct holds TopSpaceMetr PM = TopStruct (#the carrier of PM, Family_open_set(PM)#); theorem :: CARDFIL3:21 for PM being MetrStruct holds the carrier of TopStruct (#the carrier of PM, Family_open_set(PM)#) = the carrier of PM; theorem :: CARDFIL3:22 for PM being MetrStruct holds the carrier of TopSpaceMetr PM = the carrier of TopStruct (#the carrier of PM, Family_open_set(PM)#); theorem :: CARDFIL3:23 for PM being MetrStruct holds the carrier of TopSpaceMetr PM = the carrier of PM; theorem :: CARDFIL3:24 for N being RealNormSpace, s being sequence of the carrier of TopSpaceMetr MetricSpaceNorm N, j being Nat holds s.j is Element of the carrier of TopSpaceMetr MetricSpaceNorm N; definition let N being RealNormSpace, x be Point of TopSpaceMetr MetricSpaceNorm N; func #x -> Point of N equals :: CARDFIL3:def 3 x; end; theorem :: CARDFIL3:25 for N being RealNormSpace, s being sequence of the carrier of TopSpaceMetr MetricSpaceNorm N, x being Point of TopSpaceMetr MetricSpaceNorm N holds x in lim_f s iff (for n being positive Nat ex i be Nat st for j being Nat st i <= j holds ||.#x- #(s.j) .|| < 1/n); begin :: Convergence in LinearTopSpace theorem :: CARDFIL3:26 for X being non empty LinearTopSpace holds NeighborhoodSystem 0.X is local_base of X; theorem :: CARDFIL3:27 for X being LinearTopSpace, O being local_base of X, a being Point of X, P being Subset-Family of X st P = {a+U where U is Subset of X: U in O} holds P is basis of a; theorem :: CARDFIL3:28 for X being non empty LinearTopSpace, x being Point of X, O being local_base of X holds {x+U where U is Subset of X:U in O & U is a_neighborhood of 0.X} = {x+U where U is Subset of X:U in O & U in NeighborhoodSystem 0.X}; theorem :: CARDFIL3:29 for X being non empty LinearTopSpace, x being Point of X, O being local_base of X, B being Subset-Family of X st B = {x+U where U is Subset of X:U in O & U is a_neighborhood of 0.X} holds B is basis of BOOL2F NeighborhoodSystem x; theorem :: CARDFIL3:30 for X being non empty LinearTopSpace, s being sequence of the carrier of X, x being Point of X, V being local_base of X, B being Subset-Family of X st B={x+U where U is Subset of X:U in V & U is a_neighborhood of 0.X} holds x in lim_f s iff for v being Element of B holds ex i being Nat st for j being Nat st i <=j holds s.j in v; theorem :: CARDFIL3:31 for X being non empty LinearTopSpace, s being sequence of the carrier of X, x being Point of X, V being local_base of X holds x in lim_f s iff for v being Subset of X st v in (V /\ NeighborhoodSystem 0.X) holds ex i being Nat st for j being Nat st i <= j holds s.j in x+v; theorem :: CARDFIL3:32 for T being non empty LinearTopSpace, L being non empty transitive reflexive RelStr, f being Function of [#]L,the carrier of T, x being Point of T, B being basis of BOOL2F NeighborhoodSystem x st [#]L is directed holds x in lim_f f iff for b being Element of B ex i be Element of L st for j being Element of L st i <=j holds f.j in b; theorem :: CARDFIL3:33 for T being non empty LinearTopSpace, L being non empty transitive reflexive RelStr, f being Function of [#]L,the carrier of T, x being Point of T, V being local_base of T st [#]L is directed holds x in lim_f f iff (for v being Subset of T st v in (V/\NeighborhoodSystem 0.T) ex i being Element of L st for j being Element of L st i <=j holds f.j in x+v); begin :: Partial sum in Abgroup (Abelian AddGroup) definition let I being non empty set, L being AbGroup, x being (the carrier of L)-valued ManySortedSet of I, J being Element of Fin I; func Sum(x,J) ->Element of L means :: CARDFIL3:def 4 ex p being one-to-one FinSequence of I st rng p = J & it = (the addF of L) "**" #(p,x); end; theorem :: CARDFIL3:34 for I being non empty set, L being AbGroup, x being (the carrier of L)-valued ManySortedSet of I, J being Element of Fin I holds for e being Element of Fin I st e={} holds Sum(x,e)=0.L & for e,f being Element of Fin I st e misses f holds Sum(x,e\/f)=Sum(x,e)+Sum(x,f); definition let I be non empty set, L be AbGroup, x be (the carrier of L)-valued ManySortedSet of I; func Partial_Sums(x) -> Function of [#]OrderedFIN I,the carrier of L means :: CARDFIL3:def 5 for j being Element of Fin I holds it.j = Sum(x,j); end; begin :: Product of family as limit in commutative Topological Group definition let I be non empty set, L be commutative TopGroup, x be (the carrier of L)-valued ManySortedSet of I, J be Element of Fin I; func Product(x,J) -> Element of L means :: CARDFIL3:def 6 ex p being one-to-one FinSequence of I st rng p = J & it = (the multF of L) "**" #(p,x); end; theorem :: CARDFIL3:35 for I being set, G being TopGroup, f being Function of [#]OrderedFIN I,the carrier of G, x being Point of G, B being basis of BOOL2F NeighborhoodSystem x holds x in lim_f f iff for b being Element of B ex i be Element of OrderedFIN I st for j being Element of OrderedFIN I st i <= j holds f.j in b; theorem :: CARDFIL3:36 for I being non empty set, L being commutative TopGroup, x being (the carrier of L)-valued ManySortedSet of I, J being Element of Fin I holds for e being Element of Fin I st e={} holds Product(x,e)=1_L & for e,f being Element of Fin I st e misses f holds Product(x,e\/f)=Product(x,e) * Product(x,f); definition let I be non empty set, L be commutative TopGroup, x be (the carrier of L)-valued ManySortedSet of I; func Partial_Product(x) -> Function of [#]OrderedFIN I,the carrier of L means :: CARDFIL3:def 7 for j being Element of Fin I holds it.j=Product(x,j); end; theorem :: CARDFIL3:37 for I being non empty set, G being commutative TopGroup, s being (the carrier of G)-valued ManySortedSet of I, x being Point of G, B being basis of BOOL2F NeighborhoodSystem x holds x in lim_f Partial_Product(s) iff for b being Element of B ex i be Element of OrderedFIN I st for j being Element of OrderedFIN I st i <= j holds (Partial_Product(s)).j in b; begin :: Summable family in commutative topological group definition let I be non empty set, L be Abelian TopaddGroup, x be (the carrier of L)-valued ManySortedSet of I, J be Element of Fin I; func Sum(x,J) -> Element of L means :: CARDFIL3:def 8 ex p being one-to-one FinSequence of I st rng p = J & it = (the addF of L) "**" #(p,x); end; theorem :: CARDFIL3:38 for I being set, G being TopaddGroup, f being Function of [#]OrderedFIN I,the carrier of G, x being Point of G, B being basis of BOOL2F NeighborhoodSystem x holds x in lim_f f iff for b being Element of B ex i being Element of OrderedFIN I st for j being Element of OrderedFIN I st i <= j holds f.j in b; theorem :: CARDFIL3:39 for I being non empty set, L being Abelian TopaddGroup, x being (the carrier of L)-valued ManySortedSet of I, J being Element of Fin I holds for e being Element of Fin I st e={} holds Sum(x,e)=0_L & for e,f being Element of Fin I st e misses f holds Sum(x,e\/f)=Sum(x,e) + Sum(x,f); definition let I be non empty set, L be Abelian TopaddGroup, x be (the carrier of L)-valued ManySortedSet of I; func Partial_Sums(x) -> Function of [#]OrderedFIN I,the carrier of L means :: CARDFIL3:def 9 for j being Element of Fin I holds it.j=Sum(x,j); end; theorem :: CARDFIL3:40 for I being non empty set, G being Abelian TopaddGroup, s being (the carrier of G)-valued ManySortedSet of I, x being Point of G, B being basis of BOOL2F NeighborhoodSystem x holds x in lim_f Partial_Sums(s) iff for b being Element of B ex i being Element of OrderedFIN I st for j being Element of OrderedFIN I st i <= j holds (Partial_Sums(s)).j in b;