:: Summable Family in a Commutative Group
:: by Roland Coghetto
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem :: CARDFIL3:1

for I being set holds {} is Element of Fin I

proof end;

theorem Th1: :: 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 )

proof end;

theorem Th2: :: CARDFIL3:3

for I being set
for Y being non empty set
for x being b₂ -valued ManySortedSet of I
for p being FinSequence of I holds p * x is FinSequence of Y

proof end;

theorem Th3: :: CARDFIL3:4

for I, X being non empty set
for x being b₂ -valued ManySortedSet of I
for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)

proof end;

definition

let I be set ;
let Y be non empty set ;
let x be Y -valued ManySortedSet of I;
let p be FinSequence of I;

func # (p,x) -> FinSequence of Y equals :: CARDFIL3:def 1
p * x;

coherence
p * x is FinSequence of Y by Th2;

end;

:: deftheorem defines # CARDFIL3:def 1 :
for I being set
for Y being non empty set
for x being b₂ -valued ManySortedSet of I
for p being FinSequence of I holds # (p,x) = p * x;

definition

let I be set ;

func OrderedFIN I -> non empty reflexive transitive RelStr equals :: CARDFIL3:def 2
InclPoset (Fin I);

coherence
InclPoset (Fin I) is non empty reflexive transitive RelStr ;

end;

:: deftheorem defines OrderedFIN CARDFIL3:def 2 :
for I being set holds OrderedFIN I = InclPoset (Fin I);

theorem Th4: :: CARDFIL3:5

for I being set holds [#] (OrderedFIN I) is directed

proof end;

theorem Th5: :: CARDFIL3:6

for M being non empty MetrSpace
for x being Point of (TopSpaceMetr M) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x))

proof end;

theorem :: CARDFIL3:7

for M being non empty MetrSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of (TopSpaceMetr M)
for x being Point of (TopSpaceMetr M)
for 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 ) by CARDFIL2:84;

theorem :: CARDFIL3:8

for M being non empty MetrSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of (TopSpaceMetr M)
for 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 )

proof end;

theorem Th6: :: CARDFIL3:9

for M being non empty MetrSpace
for s being sequence of the carrier of (TopSpaceMetr M)
for 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 )

proof end;

theorem Th7: :: CARDFIL3:10

for T being non empty TopStruct
for s being sequence of T
for x being Point of T holds
( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
s . m in U1 )

proof end;

theorem Th8: :: CARDFIL3:11

for M being non empty MetrSpace
for s being sequence of the carrier of (TopSpaceMetr M)
for 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 )

proof end;

theorem :: CARDFIL3:12

for M being non empty MetrSpace
for s being sequence of the carrier of (TopSpaceMetr M)
for x being Point of (TopSpaceMetr M) holds
( x in lim_f s iff x in Lim s )

proof end;

theorem :: CARDFIL3:13

for N being RealNormSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for x being Point of (TopSpaceMetr (MetricSpaceNorm N))
for 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 ) by CARDFIL2:84;

theorem :: CARDFIL3:14

for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;

theorem :: CARDFIL3:15

for N being RealNormSpace
for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for 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 ) by Th6;

theorem :: CARDFIL3:16

for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) ex y being Point of (MetricSpaceNorm N) st
( y = x & Balls x = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) by FRECHET:def 1;

theorem :: CARDFIL3:17

for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N))
for y being Point of (MetricSpaceNorm N)
for n being positive Nat st x = y holds
Ball (y,(1 / n)) in Balls x

proof end;

theorem :: CARDFIL3:18

for N being RealNormSpace
for x being Point of (MetricSpaceNorm N)
for n being Nat st n <> 0 holds
Ball (x,(1 / n)) = { q where q is Element of (MetricSpaceNorm N) : dist (x,q) < 1 / n } by METRIC_1:def 14;

theorem :: CARDFIL3:19

for N being RealNormSpace
for x being Element of (MetricSpaceNorm N)
for 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 } ) by NORMSP_2:2;

theorem :: CARDFIL3:20

for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;

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) #) by PCOMPS_1:def 5;

theorem Th9: :: CARDFIL3:23

for PM being MetrStruct holds the carrier of (TopSpaceMetr PM) = the carrier of PM

proof end;

theorem :: CARDFIL3:24

for N being RealNormSpace
for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for j being Nat holds s . j is Element of the carrier of (TopSpaceMetr (MetricSpaceNorm N)) ;

definition

let N be RealNormSpace;
let x be Point of (TopSpaceMetr (MetricSpaceNorm N));

func # x -> Point of N equals :: CARDFIL3:def 3
x;

coherence
x is Point of N

proof end;

end;

:: deftheorem defines # CARDFIL3:def 3 :
for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds # x = x;

theorem :: CARDFIL3:25

for N being RealNormSpace
for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds
( x in lim_f s iff for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n )

proof end;

theorem :: CARDFIL3:26

for X being LinearTopSpace holds NeighborhoodSystem (0. X) is local_base of X

proof end;

Lm1: for X being non empty addLoopStr
for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M

proof end;

Lm2: for X being LinearTopSpace
for x being Point of X
for 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 ) } is non empty Subset-Family of X

proof end;

theorem :: CARDFIL3:27

for X being LinearTopSpace
for O being local_base of X
for a being Point of X
for 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

proof end;

theorem :: CARDFIL3:28

for X being LinearTopSpace
for x being Point of X
for 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) ) }

proof end;

theorem Th10: :: CARDFIL3:29

for X being LinearTopSpace
for x being Point of X
for O being local_base of X
for 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))

proof end;

theorem :: CARDFIL3:30

for X being LinearTopSpace
for s being sequence of the carrier of X
for x being Point of X
for V being local_base of X
for 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 ex i being Nat st
for j being Nat st i <= j holds
s . j in v )

proof end;

theorem :: CARDFIL3:31

for X being LinearTopSpace
for s being sequence of the carrier of X
for x being Point of X
for 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 )

proof end;

theorem :: CARDFIL3:32

for T being LinearTopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for 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 ) by CARDFIL2:84;

Lm3: for T being LinearTopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for V being local_base of T
for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } 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 )

proof end;

theorem :: CARDFIL3:33

for T being LinearTopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for 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)) holds
ex i being Element of L st
for j being Element of L st i <= j holds
f . j in x + v )

proof end;

definition

let I be non empty set ;
let L be AbGroup;
let x be the carrier of L -valued ManySortedSet of I;
let J be Element of Fin I;

func Sum (x,J) -> Element of L means :Def1: :: CARDFIL3:def 4
ex p being one-to-one FinSequence of I st
( rng p = J & it = the addF of L "**" (# (p,x)) );

existence
ex b₁ being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the addF of L "**" (# (p,x)) )

proof end;

uniqueness
for b₁, b₂ being Element of L st ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & b₂ = the addF of L "**" (# (p,x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Sum CARDFIL3:def 4 :
for I being non empty set
for L being AbGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J being Element of Fin I
for b₅ being Element of L holds
( b₅ = Sum (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b₅ = the addF of L "**" (# (p,x)) ) );

theorem :: CARDFIL3:34

for I being non empty set
for L being AbGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J, 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)) ) )

proof end;

definition

let I be non empty set ;
let L be AbGroup;
let 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);

existence
ex b₁ being Function of ([#] (OrderedFIN I)), the carrier of L st
for j being Element of Fin I holds b₁ . j = Sum (x,j)

proof end;

uniqueness
for b₁, b₂ being Function of ([#] (OrderedFIN I)), the carrier of L st ( for j being Element of Fin I holds b₁ . j = Sum (x,j) ) & ( for j being Element of Fin I holds b₂ . j = Sum (x,j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Partial_Sums CARDFIL3:def 5 :
for I being non empty set
for L being AbGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for b₄ being Function of ([#] (OrderedFIN I)), the carrier of L holds
( b₄ = Partial_Sums x iff for j being Element of Fin I holds b₄ . j = Sum (x,j) );

definition

let I be non empty set ;
let L be commutative TopGroup;
let x be the carrier of L -valued ManySortedSet of I;
let J be Element of Fin I;

func Product (x,J) -> Element of L means :Def2: :: CARDFIL3:def 6
ex p being one-to-one FinSequence of I st
( rng p = J & it = the multF of L "**" (# (p,x)) );

existence
ex b₁ being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the multF of L "**" (# (p,x)) )

proof end;

uniqueness
for b₁, b₂ being Element of L st ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the multF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & b₂ = the multF of L "**" (# (p,x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Product CARDFIL3:def 6 :
for I being non empty set
for L being commutative TopGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J being Element of Fin I
for b₅ being Element of L holds
( b₅ = Product (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b₅ = the multF of L "**" (# (p,x)) ) );

theorem Th11: :: CARDFIL3:35

for I being set
for G being TopGroup
for f being Function of ([#] (OrderedFIN I)), the carrier of G
for x being Point of G
for 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 )

proof end;

theorem :: CARDFIL3:36

for I being non empty set
for L being commutative TopGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J, 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)) ) )

proof end;

definition

let I be non empty set ;
let L be commutative TopGroup;
let 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);

existence
ex b₁ being Function of ([#] (OrderedFIN I)), the carrier of L st
for j being Element of Fin I holds b₁ . j = Product (x,j)

proof end;

uniqueness
for b₁, b₂ being Function of ([#] (OrderedFIN I)), the carrier of L st ( for j being Element of Fin I holds b₁ . j = Product (x,j) ) & ( for j being Element of Fin I holds b₂ . j = Product (x,j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Partial_Product CARDFIL3:def 7 :
for I being non empty set
for L being commutative TopGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for b₄ being Function of ([#] (OrderedFIN I)), the carrier of L holds
( b₄ = Partial_Product x iff for j being Element of Fin I holds b₄ . j = Product (x,j) );

theorem :: CARDFIL3:37

for I being non empty set
for G being commutative TopGroup
for s being the carrier of b₂ -valued ManySortedSet of I
for x being Point of G
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f (Partial_Product 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_Product s) . j in b ) by Th11;

definition

let I be non empty set ;
let L be Abelian TopaddGroup;
let x be the carrier of L -valued ManySortedSet of I;
let J be Element of Fin I;

func Sum (x,J) -> Element of L means :Def3: :: CARDFIL3:def 8
ex p being one-to-one FinSequence of I st
( rng p = J & it = the addF of L "**" (# (p,x)) );

existence
ex b₁ being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the addF of L "**" (# (p,x)) )

proof end;

uniqueness
for b₁, b₂ being Element of L st ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & b₂ = the addF of L "**" (# (p,x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Sum CARDFIL3:def 8 :
for I being non empty set
for L being Abelian TopaddGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J being Element of Fin I
for b₅ being Element of L holds
( b₅ = Sum (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b₅ = the addF of L "**" (# (p,x)) ) );

theorem Th12: :: CARDFIL3:38

for I being set
for G being TopaddGroup
for f being Function of ([#] (OrderedFIN I)), the carrier of G
for x being Point of G
for 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 )

proof end;

theorem :: CARDFIL3:39

for I being non empty set
for L being Abelian TopaddGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J, 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)) ) )

proof end;

definition

let I be non empty set ;
let L be Abelian TopaddGroup;
let 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);

existence
ex b₁ being Function of ([#] (OrderedFIN I)), the carrier of L st
for j being Element of Fin I holds b₁ . j = Sum (x,j)

proof end;

uniqueness
for b₁, b₂ being Function of ([#] (OrderedFIN I)), the carrier of L st ( for j being Element of Fin I holds b₁ . j = Sum (x,j) ) & ( for j being Element of Fin I holds b₂ . j = Sum (x,j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Partial_Sums CARDFIL3:def 9 :
for I being non empty set
for L being Abelian TopaddGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for b₄ being Function of ([#] (OrderedFIN I)), the carrier of L holds
( b₄ = Partial_Sums x iff for j being Element of Fin I holds b₄ . j = Sum (x,j) );

theorem :: CARDFIL3:40

for I being non empty set
for G being Abelian TopaddGroup
for s being the carrier of b₂ -valued ManySortedSet of I
for x being Point of G
for 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 ) by Th12;