:: Summable Family in a Commutative Group
:: by Roland Coghetto
::
:: 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 b2 -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 b2 -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 b2 -valued ManySortedSet of I
for p being FinSequence of I holds # (p,x) = p * x;

definition
let I be set ;
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 [#] () is directed
proof end;

theorem Th5: :: CARDFIL3:6
for M being non empty MetrSpace
for x being Point of () holds Balls x is basis of ()
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 ()
for x being Point of ()
for B being basis of () 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 ()
for x being Point of () 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 ()
for x being Point of () 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 ()
for x being Point of () 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 ()
for x being Point of () 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 ()
for x being Point of ()
for B being basis of () 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 () holds Balls x is basis of () by Th5;

theorem :: CARDFIL3:15
for N being RealNormSpace
for s being sequence of the carrier of ()
for x being Point of () 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 () ex y being Point of () 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 ()
for y being Point of ()
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 ()
for n being Nat st n <> 0 holds
Ball (x,(1 / n)) = { q where q is Element of () : dist (x,q) < 1 / n } by METRIC_1:def 14;

theorem :: CARDFIL3:19
for N being RealNormSpace
for x being Element of ()
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,() #) by PCOMPS_1:def 5;

theorem :: CARDFIL3:21
for PM being MetrStruct holds the carrier of TopStruct(# the carrier of PM,() #) = the carrier of PM ;

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

theorem Th9: :: CARDFIL3:23
for PM being MetrStruct holds the carrier of () = the carrier of PM
proof end;

theorem :: CARDFIL3:24
for N being RealNormSpace
for s being sequence of the carrier of ()
for j being Nat holds s . j is Element of the carrier of () ;

definition
let N be RealNormSpace;
let x be Point of ();
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 () holds # x = x;

theorem :: CARDFIL3:25
for N being RealNormSpace
for s being sequence of the carrier of ()
for x being Point of () 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 ()
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 /\ () 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 () 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 /\ () 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 b1 being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b1 = the addF of L "**" (# (p,x)) )
proof end;
uniqueness
for b1, b2 being Element of L st ex p being one-to-one FinSequence of I st
( rng p = J & b1 = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & b2 = the addF of L "**" (# (p,x)) ) holds
b1 = b2
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 b2 -valued ManySortedSet of I
for J being Element of Fin I
for b5 being Element of L holds
( b5 = Sum (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b5 = 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 b2 -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 ([#] ()), the carrier of L means :: CARDFIL3:def 5
for j being Element of Fin I holds it . j = Sum (x,j);
existence
ex b1 being Function of ([#] ()), the carrier of L st
for j being Element of Fin I holds b1 . j = Sum (x,j)
proof end;
uniqueness
for b1, b2 being Function of ([#] ()), the carrier of L st ( for j being Element of Fin I holds b1 . j = Sum (x,j) ) & ( for j being Element of Fin I holds b2 . j = Sum (x,j) ) holds
b1 = b2
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 b2 -valued ManySortedSet of I
for b4 being Function of ([#] ()), the carrier of L holds
( b4 = Partial_Sums x iff for j being Element of Fin I holds b4 . 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 b1 being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b1 = the multF of L "**" (# (p,x)) )
proof end;
uniqueness
for b1, b2 being Element of L st ex p being one-to-one FinSequence of I st
( rng p = J & b1 = the multF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & b2 = the multF of L "**" (# (p,x)) ) holds
b1 = b2
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 b2 -valued ManySortedSet of I
for J being Element of Fin I
for b5 being Element of L holds
( b5 = Product (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b5 = the multF of L "**" (# (p,x)) ) );

theorem Th11: :: CARDFIL3:35
for I being set
for G being TopGroup
for f being Function of ([#] ()), the carrier of G
for x being Point of G
for B being basis of () holds
( x in lim_f f iff for b being Element of B ex i being Element of () st
for j being Element of () 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 b2 -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 ([#] ()), the carrier of L means :: CARDFIL3:def 7
for j being Element of Fin I holds it . j = Product (x,j);
existence
ex b1 being Function of ([#] ()), the carrier of L st
for j being Element of Fin I holds b1 . j = Product (x,j)
proof end;
uniqueness
for b1, b2 being Function of ([#] ()), the carrier of L st ( for j being Element of Fin I holds b1 . j = Product (x,j) ) & ( for j being Element of Fin I holds b2 . j = Product (x,j) ) holds
b1 = b2
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 b2 -valued ManySortedSet of I
for b4 being Function of ([#] ()), the carrier of L holds
( b4 = Partial_Product x iff for j being Element of Fin I holds b4 . j = Product (x,j) );

theorem :: CARDFIL3:37
for I being non empty set
for G being commutative TopGroup
for s being the carrier of b2 -valued ManySortedSet of I
for x being Point of G
for B being basis of () holds
( x in lim_f () iff for b being Element of B ex i being Element of () st
for j being Element of () st i <= j holds
() . j in b ) by Th11;

definition
let I be non empty set ;
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 b1 being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b1 = the addF of L "**" (# (p,x)) )
proof end;
uniqueness
for b1, b2 being Element of L st ex p being one-to-one FinSequence of I st
( rng p = J & b1 = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & b2 = the addF of L "**" (# (p,x)) ) holds
b1 = b2
proof end;
end;

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

theorem Th12: :: CARDFIL3:38
for I being set
for f being Function of ([#] ()), the carrier of G
for x being Point of G
for B being basis of () holds
( x in lim_f f iff for b being Element of B ex i being Element of () st
for j being Element of () st i <= j holds
f . j in b )
proof end;

theorem :: CARDFIL3:39
for I being non empty set
for x being the carrier of b2 -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 x be the carrier of L -valued ManySortedSet of I;
func Partial_Sums x -> Function of ([#] ()), the carrier of L means :: CARDFIL3:def 9
for j being Element of Fin I holds it . j = Sum (x,j);
existence
ex b1 being Function of ([#] ()), the carrier of L st
for j being Element of Fin I holds b1 . j = Sum (x,j)
proof end;
uniqueness
for b1, b2 being Function of ([#] ()), the carrier of L st ( for j being Element of Fin I holds b1 . j = Sum (x,j) ) & ( for j being Element of Fin I holds b2 . j = Sum (x,j) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Partial_Sums CARDFIL3:def 9 :
for I being non empty set