:: Summable Family in a Commutative Group
:: by Roland Coghetto
::
:: Received August 14, 2015
:: Copyright (c) 2015-2026 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;
definitions YELLOW13;
equalities ORDINAL1, ALGSTR_0;
expansions TARSKI, FRECHET, XBOOLE_0, FUNCT_1, RELAT_1, CARDFIL2;
theorems GROUP_1A, FRECHET, CONNSP_2, YELLOW_8, YELLOW19, TOPMETR, METRIC_1,
NORMSP_2, PCOMPS_1, RLTOPSP1, YELLOW13, XBOOLE_0, RUSUB_4, CARD_FIL,
RLVECT_1, TOPS_1, TOPGRP_1, FINSUB_1, FINSEQ_1, FINSOP_1, FINSEQ_4,
BHSP_5, FVSUM_1, RELAT_1, TARSKI, XBOOLE_1, FUNCT_1, FINSEQ_2, FINSEQ_3,
FUNCT_2, PARTFUN1, STRUCT_0, WAYBEL_0, YELLOW_1, GROUP_1, CARDFIL2;
schemes FUNCT_2, BINOP_2;
begin :: Preliminaries
theorem
for I being set holds {} is Element of Fin I
proof
let I be set;
A1: Fin {} c= Fin I by XBOOLE_1:2,FINSUB_1:10;
{} in {{}} by TARSKI:def 1;
hence thesis by A1,FINSUB_1:15;
end;
theorem Th1:
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
let I, J be set such that
A1: J in Fin I;
consider p be FinSequence such that
A2: J = rng p & p is one-to-one by A1,FINSEQ_4:58;
rng p c= I by A1,A2,FINSUB_1:def 5;
then reconsider p as FinSequence of I by FINSEQ_1:def 4;
take p;
thus thesis by A2;
end;
theorem Th2:
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
proof
let I be set, Y be non empty set,
x be Y-valued ManySortedSet of I,
p be FinSequence of I;
A1: dom x =I by PARTFUN1:def 2;
A2: rng x c= Y by RELAT_1:def 19;
then
A3: x is Function of I,Y by A1,FUNCT_2:2;
reconsider x1=x as Function of I,Y by A1,A2,FUNCT_2:2;
reconsider xp=p*x1 as FinSequence;
thus thesis by A3,FINSEQ_2:32;
end;
theorem Th3:
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)
proof
let I,X be non empty set,
x be X-valued ManySortedSet of I,
p,q be FinSequence of I;
A1: dom x =I by PARTFUN1:def 2;
rng x c= X by RELAT_1:def 19; then
A2: x is Function of I,X by A1,FUNCT_2:2; then
A3: dom (p * x)=dom p & dom (q*x)=dom q &
dom ((p^q)*x)=dom (p^q) by FINSEQ_3:120;
A4: dom (p^q)=Seg (len p + len q) by FINSEQ_1:def 7;
A5: Seg len(p*x)=dom p & Seg len(q*x)=dom q by A3,FINSEQ_1:def 3;
A6: len (p*x)=len p & len (q*x)=len q by A5,FINSEQ_1:def 3; then
A7: dom ((p*x) ^ (q*x))= Seg(len p+len q) by FINSEQ_1:def 7;
for t be object st t in dom ((p^q)*x) holds
((p^q) * x).t = ((p * x) ^ (q * x)).t
proof
let t be object;
assume
A8: t in dom((p^q)*x);
A9: t in dom(p^q) by A2,FINSEQ_3:120,A8;
A10: ((p^q) * x).t=x.((p^q).t) by A2,FINSEQ_3:120,A8;
now
hereby
assume
A11: t in dom p;
then
A12: x.((p^q).t) =x.(p.t) &
x.(p.t) = (p*x).t by FINSEQ_1:def 7,FUNCT_1:13;
t in dom (p *x ) by A11,A2,FINSEQ_3:120;
hence ((p^q) * x).t=((p * x) ^ (q * x)).t
by A12,A10,FINSEQ_1:def 7;
end;
assume ex n be Nat st n in dom q & t=len p + n;
then consider n be Nat such that
A13: n in dom q and
A14: t=len p + n;
A15: x.((p^q).(len p + n))=x.(q.n) by A13,FINSEQ_1:def 7;
n in dom (q*x) by A13,A2,FINSEQ_3:120;
then ((p * x) ^ (q * x)).(len p + n)=(q * x).n by A6,FINSEQ_1:def 7;
hence ((p^q) * x).t=((p * x) ^ (q * x)).t
by A13,A14,A15,A10,FUNCT_1:13;
end;
hence thesis by A9,FINSEQ_1:25;
end;
hence thesis by A7,A2,FINSEQ_3:120,A4;
end;
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 p*x;
coherence by Th2;
end;
definition
let I being set;
func OrderedFIN I -> non empty transitive reflexive RelStr equals
InclPoset Fin I;
coherence;
end;
theorem Th4:
for I being set holds [#]OrderedFIN I is directed
proof
let I be set;
A1: the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then
A2: [#]OrderedFIN I= Fin I by STRUCT_0:def 3;
now
let a,b be Element of OrderedFIN I;
assume that
a in [#]OrderedFIN I and
b in [#]OrderedFIN I;
reconsider z=a\/b as Element of OrderedFIN I by A1,FINSUB_1:def 1;
take z;
thus z in [#]OrderedFIN I &
a <= z & b <= z by A1,A2,YELLOW_1:3,XBOOLE_1:7;
end;
hence thesis by WAYBEL_0:def 1;
end;
begin :: Convergence in TopSpaceMetr
theorem Th5:
for M being non empty MetrSpace,
x being Point of TopSpaceMetr(M)
holds Balls(x) is basis of BOOL2F NeighborhoodSystem x
proof
let M be non empty MetrSpace,x be Point of TopSpaceMetr(M);
set F=BOOL2F NeighborhoodSystem x;
now
let t be object;
assume
A1: t in Balls(x);
then reconsider t1=t as Subset of TopSpaceMetr(M);
consider y being Point of M such that
A2: y=x and
A3: Balls(x)= { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1;
consider n0 be Nat such that
A4: t=Ball(y,1/n0) and
A5: n0 <> 0 by A1,A3;
reconsider r0=1/n0 as Real;
A6: 0 <r0 by A5;
dist(y,y)<r0 by A6,METRIC_1:1; then
A7: y in {q where q is Element of M:dist (y,q) < r0};
t1 is open & x in t1 by A7,A4,TOPMETR:14,A2,METRIC_1:def 14;
then t1 is a_neighborhood of x by CONNSP_2:3;
then t in NeighborhoodSystem x by YELLOW19:2;
hence t in F by CARDFIL2:def 20;
end;
then Balls(x) c= F;
then reconsider BAX = Balls(x) as non empty Subset of F;
now
let f be Element of F;
f in BOOL2F NeighborhoodSystem x;
then f in NeighborhoodSystem x by CARDFIL2:def 20;
then f is a_neighborhood of x by YELLOW19:2;
then consider V being Subset of TopSpaceMetr(M) such that
A8: V is open & V c= f & x in V by CONNSP_2:6;
consider b being Subset of TopSpaceMetr(M) such that
A9: b in Balls(x) & b c= V by A8,YELLOW_8:def 1;
reconsider b as Element of BAX by A9;
take b;
thus b c= f by A8,A9;
end;
then BAX is filter_basis;
hence thesis;
end;
theorem
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 by CARDFIL2:84;
theorem
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
proof
let M be non empty MetrSpace,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,the carrier of TopSpaceMetr(M),
x be Point of TopSpaceMetr(M);
assume
A1: [#]L is directed;
Balls(x) is basis of BOOL2F NeighborhoodSystem x by Th5;
hence thesis by A1,CARDFIL2:84;
end;
theorem Th6:
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
proof
let M be non empty MetrSpace,
s be sequence of the carrier of TopSpaceMetr(M),
x be Point of TopSpaceMetr(M);
Balls(x) is basis of BOOL2F NeighborhoodSystem x by Th5;
hence thesis by CARDFIL2:97;
end;
theorem Th7:
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
proof
let T be non empty TopStruct,s be sequence of T,
x be Point of T;
x in Lim s iff s is_convergent_to x by FRECHET:def 5;
hence thesis;
end;
theorem Th8:
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
proof
let M be non empty MetrSpace,
s be sequence of the carrier of TopSpaceMetr(M),
x be Point of TopSpaceMetr(M);
now
hereby
assume
A1: x in Lim s;
now
let b be Element of Balls(x);
Balls(x) is basis of BOOL2F NeighborhoodSystem x by Th5;
then Balls(x) c= BOOL2F NeighborhoodSystem x;
then b in BOOL2F NeighborhoodSystem x;
then b in NeighborhoodSystem x by CARDFIL2:def 20;
then b is a_neighborhood of x by YELLOW19:2;
then consider V being Subset of TopSpaceMetr(M) such that
A2: V is open and
A3: V c= b and
A4: x in V by CONNSP_2:6;
consider n0 being Nat such that
A5: for m being Nat st n0 <= m holds s.m in V by A2,A4,A1,Th7;
take n0;
thus for m being Nat st n0 <= m holds s.m in b by A3,A5;
end;
hence x in Lim s implies
for b be Element of Balls(x)
ex n being Nat st
for m being Nat st n <= m holds s.m in b;
end;
assume
A6: for b be Element of Balls(x)
ex n being Nat st for m being Nat st n <= m holds s.m in b;
now
let U1 be Subset of TopSpaceMetr(M);
assume U1 is open & x in U1;
then U1 is a_neighborhood of x by CONNSP_2:6;
then U1 in NeighborhoodSystem x by YELLOW19:2;
then
A7: U1 is Element of BOOL2F NeighborhoodSystem x by CARDFIL2:def 20;
reconsider BAX=Balls(x) as
non empty Subset of BOOL2F NeighborhoodSystem x by Th5;
BAX is filter_basis by Th5;
then consider b be Element of Balls(x) such that
A8: b c= U1 by A7;
consider n0 being Nat such that
A9: for m being Nat st n0 <= m holds s.m in b by A6;
take n0;
thus for m being Nat st n0 <= m holds s.m in U1 by A9,A8;
end;
hence x in Lim s by Th7;
end;
hence thesis;
end;
theorem
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
proof
let M be non empty MetrSpace,
s be sequence of the carrier of TopSpaceMetr(M),
x be Point of TopSpaceMetr(M);
hereby
assume x in lim_f s;
then for b be Element of Balls(x) ex i be Nat st
for j be Nat st i <=j holds s.j in b by Th6;
hence x in Lim s by Th8;
end;
assume x in Lim s;
then for b be Element of Balls(x) ex i be Nat st
for j be Nat st i <=j holds s.j in b by Th8;
hence x in lim_f s by Th6;
end;
begin :: Convergence in RealNormSpace
theorem
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 by CARDFIL2:84;
theorem
for N being RealNormSpace,
x being Point of TopSpaceMetr MetricSpaceNorm N
holds Balls(x) is basis of BOOL2F NeighborhoodSystem x by Th5;
theorem
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 by Th6;
theorem
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} by FRECHET:def 1;
theorem
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
proof
let N be RealNormSpace, x be Point of TopSpaceMetr MetricSpaceNorm N,
y be Point of MetricSpaceNorm N,
n be positive Nat such that
A1: x=y;
set M=MetricSpaceNorm N;
consider y1 be Point of M such that
A2: y1=x and
A3: Balls x = {Ball(y1,1/n) where n is Nat:n <> 0} by FRECHET:def 1;
thus thesis by A1,A2,A3;
end;
theorem
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}
by METRIC_1:def 14;
theorem
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} by NORMSP_2:2;
theorem
for PM being MetrStruct holds
TopSpaceMetr PM = TopStruct (#the carrier of PM, Family_open_set(PM)#)
by PCOMPS_1:def 5;
theorem
for PM being MetrStruct holds
the carrier of TopStruct (#the carrier of PM, Family_open_set(PM)#) =
the carrier of PM;
theorem
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:
for PM being MetrStruct holds
the carrier of TopSpaceMetr PM = the carrier of PM
proof
let PM be MetrStruct;
the carrier of TopSpaceMetr PM=
the carrier of TopStruct (#the carrier of PM,
Family_open_set(PM)#) by PCOMPS_1:def 5;
hence thesis;
end;
theorem
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 x;
coherence
proof
MetricSpaceNorm N = MetrStruct(# the carrier of N,distance_by_norm_of N #)
by NORMSP_2:def 2;
hence x is Element of N by Th9;
end;
end;
theorem
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)
proof
let N be RealNormSpace,
s be sequence of the carrier of TopSpaceMetr MetricSpaceNorm(N),
x be Point of TopSpaceMetr MetricSpaceNorm N;
reconsider x1=x as Point of TopSpaceMetr MetricSpaceNorm N;
consider y0 be Point of MetricSpaceNorm N such that
A1: y0=x1 and
A2: Balls x1={Ball(y0,1/n) where n is Nat:n <> 0} by FRECHET:def 1;
A3: x in lim_f s implies
(for n be positive Nat ex i be Nat st
for j be Nat st i <= j holds ||.#x- #(s.j) .|| < 1/n)
proof
assume
A4: x in lim_f s;
now
let n be positive Nat;
Ball(y0,1/n) in Balls x1 by A2;
then consider i0 be Nat such that
A5: for j be Nat st i0 <= j holds s.j in Ball(y0,1/n) by A4,Th6;
A6: now
let j be Nat;
assume
A7: i0 <= j;
consider y1 be Point of N such that
A8: y0=y1 and
A9: Ball (y0,1/n)={q where q is Point of N : ||.y1 - q.|| < 1/n}
by NORMSP_2:2;
s.j in {q where q is Point of N : ||.y1 - q.|| < 1/n} by A7,A5,A9;
then consider q0 be Point of N such that
A10: s.j=q0 and
A11: ||.y1 - q0.|| < 1/n;
thus ||.#x - #(s.j).|| < 1/n by A1,A8,A10,A11;
end;
take i0;
thus for j be Nat st i0<=j holds ||.#x - #(s.j).|| < 1/n by A6;
end;
hence thesis;
end;
(for n be positive Nat ex i be Nat st for j be Nat st i<=j holds
||.#x - #(s.j).|| < 1/n) implies x in lim_f s
proof
assume
A12: for n be positive Nat ex i be Nat st
for j be Nat st i<=j holds
||.#x - #(s.j).|| < 1/n;
for b be Element of Balls(x) ex i be Nat st
for j be Nat st i <=j holds s.j in b
proof
let b be Element of Balls(x);
b in {Ball(y0,1/n) where n is Nat:n <> 0} by A2;
then consider n0 be Nat such that
A13: b=Ball(y0,1/n0) and
A14: n0 <> 0;
consider i0 be Nat such that
A15: for j be Nat st i0<=j holds ||.#x - #(s.j).|| < 1/n0 by A12,A14;
take i0;
for j be Nat st i0 <= j holds s.j in b
proof
let j be Nat;
assume i0<=j; then
A16: ||.#x1 - #(s.j).||< 1/n0 by A15;
consider y1 be Point of N such that
A17: y0=y1 and
A18: Ball (y0,1/n0)={q where q is Point of N : ||.y1 - q.|| < 1/n0}
by NORMSP_2:2;
thus s.j in b by A1,A13,A16,A17,A18;
end;
hence thesis;
end;
hence thesis by Th6;
end;
hence thesis by A3;
end;
begin :: Convergence in LinearTopSpace
theorem
for X being non empty LinearTopSpace holds
NeighborhoodSystem 0.X is local_base of X
proof
let X be non empty LinearTopSpace;
reconsider p=0.X as Point of X;
BOOL2F NeighborhoodSystem 0.X is Subset-Family of X;
then reconsider NS0 = (NeighborhoodSystem 0.X) as Subset-Family of X
by CARDFIL2:def 20;
for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in NeighborhoodSystem p & P c= A ) by YELLOW19:2;
then NS0 is basis of p by YELLOW13:def 2;
hence thesis;
end;
Lm1:
for X being non empty addLoopStr,
M being Subset of X holds
for x,y being Point of X st y in M holds x+y in x+M
proof
let X be non empty addLoopStr, M be Subset of X;
let x,y be Point of X;
x + M = {x + u where u is Point of X: u in M} by RUSUB_4:def 8;
hence thesis;
end;
Lm2:
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} is
non empty Subset-Family of X
proof
let X be non empty LinearTopSpace,
x be Point of X, O be local_base of X;
set B={x+U where U is Subset of X:U in O & U is a_neighborhood of 0.X};
now let t be object;
assume t in B;
then consider U1 be Subset of X such that
A1: t=x+U1 and
U1 in O and
U1 is a_neighborhood of 0.X;
thus t in bool the carrier of X by A1;
end;
then B c= bool the carrier of X;
then reconsider B1=B as Subset-Family of X;
A2: [#]X is a_neighborhood of 0.X by TOPGRP_1:21;
consider V being a_neighborhood of 0.X such that
A3: V in O and
V c= [#]X by A2, YELLOW13:def 2;
x+V in B1 by A3;
hence thesis;
end;
theorem
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
proof
let X be LinearTopSpace, O be basis of 0.X,
a be Point of X,
P be Subset-Family of X such that
A1: P = {a+U where U is Subset of X: U in O};
let A be a_neighborhood of a;
a in Int(A) by CONNSP_2:def 1;
then (-a) + Int(A) is a_neighborhood of 0.X by RLTOPSP1:9,CONNSP_2:3;
then consider V being a_neighborhood of 0.X such that
A2: V in O and
A3: V c= -a+Int(A) by YELLOW13:def 2;
take U = a+V;
A4: a+0.X in a+Int(V) by Lm1,CONNSP_2:def 1;
a+Int(V) c= Int(U) by RLTOPSP1:37;
hence U is a_neighborhood of a by A4,CONNSP_2:def 1;
thus U in P by A1,A2;
U c= a+(-a+Int(A)) by A3,RLTOPSP1:8;
then U c= a+(-a)+Int(A) by RLTOPSP1:6;
then U c= 0.X+Int(A) by RLVECT_1:5;
then Int(A) c= A & U c= Int(A) by RLTOPSP1:5,TOPS_1:16;
hence thesis;
end;
theorem
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}
proof
let X be non empty LinearTopSpace,
x be Point of X, O be local_base of X;
now
let t be object;
assume t in {x+U where U is Subset of X:U in O &
U is a_neighborhood of 0.X};
then consider U1 be Subset of X such that
A1: t=x+U1 and
A2: U1 in O and
A3: U1 is a_neighborhood of 0.X;
U1 in NeighborhoodSystem 0.X by A3,YELLOW19:2;
hence t in {x+U where U is Subset of X:U in O &
U in NeighborhoodSystem 0.X} by A1,A2;
end;
then
A4: {x+U where U is Subset of X:U in O & U is a_neighborhood of 0.X} c=
{x+U where U is Subset of X:U in O & U in NeighborhoodSystem 0.X};
now
let t be object;
assume t in {x+U where U is Subset of X:U in O &
U in NeighborhoodSystem 0.X};
then consider U1 be Subset of X such that
A5: t=x+U1 and
A6: U1 in O and
A7: U1 in NeighborhoodSystem 0.X;
U1 is a_neighborhood of 0.X by A7,YELLOW19:2;
hence t in {x+U where U is Subset of X:U in O &
U is a_neighborhood of 0.X} by A5,A6;
end;
then {x+U where U is Subset of X:U in O & U in NeighborhoodSystem 0.X} c=
{x+U where U is Subset of X:U in O & U is a_neighborhood of 0.X};
hence thesis by A4;
end;
theorem Th10:
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
proof
let X be non empty LinearTopSpace,
x be Point of X, O be local_base of X,B be Subset-Family of X;
assume
A1: B={x+U where U is Subset of X:U in O & U is a_neighborhood of 0.X};
set F=BOOL2F NeighborhoodSystem x;
A2: F c= <.B.]
proof
now
let t be object;
assume t in F;
then t in NeighborhoodSystem x by CARDFIL2:def 20;
then t in the set of all A where
A is a_neighborhood of x by YELLOW19:def 1;
then consider A be a_neighborhood of x such that
A3: t=A;
x in Int(A) by CONNSP_2:def 1;
then -x+Int(A) is a_neighborhood of 0.X by RLTOPSP1:9,CONNSP_2:3;
then consider V being a_neighborhood of 0.X such that
A4: V in O and
A5: V c= -x+Int(A) by YELLOW13:def 2;
set U = x+V;
A6: U in B by A1,A4;
U c= x+(-x+Int(A)) by A5,RLTOPSP1:8;
then U c= x+(-x)+Int(A) by RLTOPSP1:6;
then U c= 0.X+Int(A) by RLVECT_1:5;
then Int(A) c= A & U c= Int(A) by RLTOPSP1:5,TOPS_1:16;
then U c= A;
hence t in <.B.] by A3,A6,CARDFIL2:def 8;
end;
hence thesis;
end;
<.B.] c= F
proof
now
let t be object;
assume
A7: t in <.B.];
then reconsider t1=t as Subset of X;
consider b be Element of B such that
A8: b c= t1 by A7,CARDFIL2:def 8;
set v0 = the Element of O;
B is non empty by A1,Lm2;
then b in B;
then consider U1 be Subset of X such that
A9: b=x+U1 and
U1 in O and
A10: U1 is a_neighborhood of 0.X by A1;
reconsider t2=b as Element of B;
A11: x+0.X in x+Int(U1) by Lm1, A10,CONNSP_2:def 1;
x+Int(U1) c= Int(x+U1) by RLTOPSP1:37;
then t2 is a_neighborhood of x by A9,A11,CONNSP_2:def 1;
then t2 in the set of all A where
A is a_neighborhood of x;
then t2 in NeighborhoodSystem x by YELLOW19:def 1;
then t2 in F by CARDFIL2:def 20;
hence t in F by A8,CARD_FIL:def 1;
end;
hence thesis;
end;
hence thesis by CARDFIL2:22,A2,XBOOLE_0:def 10;
end;
theorem
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
proof
let X be non empty LinearTopSpace,
s be sequence of the carrier of X,
x be Point of X, V be local_base of X,B be
Subset-Family of X;
assume B={x+U where U is Subset of X:U in V &
U is a_neighborhood of 0.X};
then B is basis of BOOL2F NeighborhoodSystem x by Th10;
hence x in lim_f s iff
for b be Element of B ex i be Nat st
for j be Nat st i <=j holds s.j in b by CARDFIL2:97;
end;
theorem
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
proof
let X be non empty LinearTopSpace,
s be sequence of the carrier of X,
x be Point of X, V be local_base of X;
set B={x+U where U is Subset of X:U in V &
U is a_neighborhood of 0.X};
reconsider B as Subset-Family of X by Lm2;
A1: B is basis of BOOL2F NeighborhoodSystem x by Th10;
hereby
assume
A2: x in lim_f s;
let v be Subset of X;
assume v in V/\NeighborhoodSystem 0.X;
then v in V & v in NeighborhoodSystem 0.X by XBOOLE_0: def 4;
then v in V & v is a_neighborhood of 0.X by YELLOW19:2;
then x+v in B;
then reconsider b=x+v as Element of B;
consider i0 be Nat such that
A3: for j be Nat st i0 <= j holds s.j in b by A2,A1,CARDFIL2:97;
thus ex i be Nat st for j be Nat st i <=j holds s.j in x+v by A3;
end;
assume
A4: for v be Subset of X st v in (V/\NeighborhoodSystem 0.X) holds
ex i be Nat st for j be Nat st i <=j holds s.j in x+v;
for b be Element of B ex i be Nat st
for j be Nat st i <=j holds s.j in b
proof
let b be Element of B;
B is non empty by Lm2;
then b in B;
then consider U1 be Subset of X such that
A5: b=x+U1 and
A6: U1 in V and
A7: U1 is a_neighborhood of 0.X;
U1 in NeighborhoodSystem 0.X by A7,YELLOW19:2;
then U1 in (V/\NeighborhoodSystem 0.X) by A6,XBOOLE_0:def 4;
then consider i0 be Nat such that
A8: for j be Nat st i0 <= j holds s.j in x+U1 by A4;
take i0;
thus thesis by A5,A8;
end;
hence x in lim_f s by A1,CARDFIL2:97;
end;
theorem
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 by CARDFIL2:84;
Lm3:
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,
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
let T be non empty LinearTopSpace,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,the carrier of T, x be Point of T,
V be local_base of T, B being Subset-Family of T;
assume that
A1: [#]L is directed and
A2: B={x+U where U is Subset of T:U in V & U is a_neighborhood of 0.T};
reconsider B1=B as basis of BOOL2F NeighborhoodSystem x by A2,Th10;
x in lim_f f iff
for b be Element of B1 ex i be Element of L st
for j be Element of L st i <=j holds f.j in b by A1,CARDFIL2:84;
hence thesis;
end;
theorem
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)
proof
let T be non empty LinearTopSpace,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,the carrier of T,
x be Point of T, V be local_base of T;
assume
A1: [#]L is directed;
set B={x+U where U is Subset of T:U in V &
U is a_neighborhood of 0.T};
reconsider B as Subset-Family of T by Lm2;
now
hereby
assume
A2: x in lim_f f;
let v be Subset of T;
assume v in (V/\NeighborhoodSystem 0.T);
then v in V & v in NeighborhoodSystem 0.T by XBOOLE_0: def 4;
then v in V & v is a_neighborhood of 0.T by YELLOW19:2;
then x+v in B;
then reconsider b=x+v as Element of B;
consider i0 be Element of L such that
A3: for j be Element of L st i0 <= j holds f.j in b
by A1,A2,Lm3;
take i0;
thus for j be Element of L st i0 <=j holds f.j in x+v by A3;
end;
assume
A4: for v be Subset of T st v in (V/\NeighborhoodSystem 0.T)
ex i be Element of L st for j be Element of L st i <=j holds f.j in x+v;
for b be Element of B ex i be Element of L st
for j be Element of L st i <=j holds f.j in b
proof
let b be Element of B;
B is non empty by Lm2;
then b in B;
then consider U1 be Subset of T such that
A5: b=x+U1 and
A6: U1 in V and
A7: U1 is a_neighborhood of 0.T;
U1 in NeighborhoodSystem 0.T by A7,YELLOW19:2;
then U1 in (V/\NeighborhoodSystem 0.T) by A6,XBOOLE_0:def 4;
then consider i0 be Element of L such that
A8: for j be Element of L st i0 <= j holds f.j in x+U1 by A4;
take i0;
thus thesis by A5,A8;
end;
hence x in lim_f f by A1,Lm3;
end;
hence thesis;
end;
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
:Def1:
ex p being one-to-one FinSequence of I st rng p = J &
it = (the addF of L) "**" #(p,x);
existence
proof
consider p be FinSequence of I such that
A1: rng p = J & p is one-to-one by Th1;
(the addF of L) "**" #(p,x) is Element of L;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Element of L such that
A2: ex p1 be one-to-one FinSequence of I st rng p1 = J &
X1 = (the addF of L) "**" #(p1,x) and
A3: ex p2 be one-to-one FinSequence of I st rng p2 = J &
X2 = (the addF of L) "**" #(p2,x);
consider p1 be one-to-one FinSequence of I such that
A4: rng p1 = J and
A5: X1 = (the addF of L) "**" #(p1,x) by A2;
consider p2 be one-to-one FinSequence of I such that
A6: rng p2 = J and
A7: X2 = (the addF of L) "**" #(p2,x) by A3;
consider P be Permutation of dom p1 such that
A8: p2=P*p1 & dom P=dom p1 & rng P=dom p1 by A4,A6,BHSP_5:1;
P is Permutation of dom #(p1,x)
proof
dom x =I by PARTFUN1:def 2;
then rng p1 c= dom x by FINSEQ_1:def 4;
then dom (p1 * x)=dom p1 by RELAT_1:27;
hence thesis;
end;
then reconsider P as Permutation of dom #(p1,x);
#(p2,x) = P * #(p1,x)
proof
now
hereby
let t be object;
assume
A9: t in #(p2,x);
consider a,b be object such that
A10: t=[a,b] by A9,RELAT_1:def 1;
consider z be object such that
A11: [a,z] in p2 and
A12: [z,b] in x by A9,A10,RELAT_1:def 8;
consider y be object such that
A13: [a,y] in P and
A14: [y,z] in p1 by A11,A8,RELAT_1:def 8;
[a,y] in P & [y,b] in p1 * x by A13,A12,A14,RELAT_1:def 8;
hence t in P * #(p1,x) by A10,RELAT_1:def 8;
end;
let t be object;
assume
A15: t in P* #(p1,x);
consider a,b be object such that
A16: t=[a,b] by A15,RELAT_1:def 1;
consider c be object such that
A17: [a,c] in P and
A18: [c,b] in p1*x by A15,A16,RELAT_1:def 8;
consider d be object such that
A19: [c,d] in p1 and
A20: [d,b] in x by A18,RELAT_1:def 8;
[a,d] in p2 by A8,RELAT_1:def 8,A17,A19;
hence t in #(p2,x) by A16,A20,RELAT_1:def 8;
end;
hence thesis;
end;
hence thesis by A5,A7,FVSUM_1:8,FINSOP_1:7;
end;
end;
theorem
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)
proof
let I be non empty set,
L be AbGroup,
x be (the carrier of L)-valued ManySortedSet of I,
J be Element of Fin I;
A1: now
let e be Element of Fin I;
assume
A2: e={};
consider p be one-to-one FinSequence of I such that
A3: rng p = e and
A4: Sum(x,e)=(the addF of L) "**" #(p,x) by Def1;
p={} by A3,A2;
then #(p,x)={} & the addF of L is having_a_unity &
len #(p,x) =0 by FVSUM_1:8;
then Sum(x,e)=the_unity_wrt the addF of L by A4,FINSOP_1:def 1;
hence Sum(x,e)=0.L by FVSUM_1:7;
end;
now
let e,f be Element of Fin I;
assume
A5: e misses f;
consider pe be one-to-one FinSequence of I such that
A6: rng pe = e and
A7: Sum(x,e)=(the addF of L) "**" #(pe,x) by Def1;
consider pf be one-to-one FinSequence of I such that
A8: rng pf = f and
A9: Sum(x,f)=(the addF of L) "**" #(pf,x) by Def1;
reconsider pepf=pe^pf as one-to-one FinSequence of I
by A5,A6,A8,FINSEQ_3:91;
A10: #(pepf,x)=#(pe,x)^#(pf,x) by Th3;
rng pepf=e\/f by A6,A8,FINSEQ_1:31;
then Sum(x,e\/f)=(the addF of L) "**" #(pepf,x) by Def1;
hence Sum(x,e\/f)=Sum(x,e)+Sum(x,f)
by A7,A9,A10,FINSOP_1:5,FVSUM_1:8;
end;
hence thesis by A1;
end;
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
for j being Element of Fin I holds it.j = Sum(x,j);
existence
proof
deffunc F(Element of Fin I)=Sum(x,$1);
consider f be Function of Fin I,the carrier of L such that
A1: for t be Element of Fin I holds f.t=F(t)
from FUNCT_2:sch 4;
the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then
A2: [#]OrderedFIN I= Fin I by STRUCT_0:def 3;
reconsider f as Function of [#]OrderedFIN I, the carrier of L by A2;
for j be Element of Fin I holds f.j=Sum(x,j) by A1;
hence thesis;
end;
uniqueness
proof
deffunc F(Element of Fin I)=Sum(x,$1);
A3: for a,b being Function of Fin I,the carrier of L st (for q being
Element of Fin I holds a.q=F(q)) & (for q being Element of Fin I holds b.
q=F(q)) holds a=b from BINOP_2:sch 1;
let f,g be Function of [#]OrderedFIN I,the carrier of L;
assume that
A4: for j be Element of Fin I holds f.j=Sum(x,j) and
A5: for j be Element of Fin I holds g.j=Sum(x,j);
the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then [#]OrderedFIN I= Fin I by STRUCT_0:def 3;
then reconsider f,g as Function of Fin I,the carrier of L;
f=g by A3,A4,A5;
hence thesis;
end;
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
:Def2:
ex p being one-to-one FinSequence of I st rng p = J &
it = (the multF of L) "**" #(p,x);
existence
proof
consider p be FinSequence of I such that
A1: rng p = J & p is one-to-one by Th1;
(the multF of L) "**" #(p,x) is Element of L;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Element of L such that
A2: ex p1 be one-to-one FinSequence of I st rng p1 = J &
X1 = (the multF of L) "**" #(p1,x) and
A3: ex p2 be one-to-one FinSequence of I st rng p2 = J &
X2 = (the multF of L) "**" #(p2,x);
consider p1 be one-to-one FinSequence of I such that
A4: rng p1 = J and
A5: X1 = (the multF of L) "**" #(p1,x) by A2;
consider p2 be one-to-one FinSequence of I such that
A6: rng p2 = J and
A7: X2 = (the multF of L) "**" #(p2,x) by A3;
consider P be Permutation of dom p1 such that
A8: p2=P*p1 & dom P=dom p1 & rng P=dom p1 by A4,A6,BHSP_5:1;
P is Permutation of dom #(p1,x)
proof
dom x =I by PARTFUN1:def 2;
then rng p1 c= dom x by FINSEQ_1:def 4;
then dom (p1 * x)=dom p1 by RELAT_1:27;
hence thesis;
end;
then reconsider P as Permutation of dom #(p1,x);
#(p2,x) = P * #(p1,x)
proof
now
hereby
let t be object;
assume
A9: t in #(p2,x);
consider a,b be object such that
A10: t=[a,b] by A9,RELAT_1:def 1;
consider z be object such that
A11: [a,z] in p2 and
A12: [z,b] in x by A9,A10,RELAT_1:def 8;
consider y be object such that
A13: [a,y] in P and
A14: [y,z] in p1 by A11,A8,RELAT_1:def 8;
[a,y] in P & [y,b] in p1 * x by A13,A12,A14,RELAT_1:def 8;
hence t in P * #(p1,x) by A10,RELAT_1:def 8;
end;
let t be object;
assume
A15: t in P* #(p1,x);
consider a,b be object such that
A16: t=[a,b] by A15,RELAT_1:def 1;
consider c be object such that
A17: [a,c] in P and
A18: [c,b] in p1*x by A15,A16,RELAT_1:def 8;
consider d be object such that
A19: [c,d] in p1 and
A20: [d,b] in x by A18,RELAT_1:def 8;
[a,d] in p2 by A8,RELAT_1:def 8,A17,A19;
hence t in #(p2,x) by A16,A20,RELAT_1:def 8;
end;
hence thesis;
end;
hence thesis by A5,A7,FINSOP_1:7;
end;
end;
theorem Th11:
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
proof
let I be set,G be TopGroup,
f be Function of [#]OrderedFIN I,the carrier of G,
x be Point of G,
B be basis of BOOL2F NeighborhoodSystem x;
[#]OrderedFIN I is directed by Th4;
hence thesis by CARDFIL2:84;
end;
theorem
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)
proof
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;
A1: now
let e be Element of Fin I;
assume
A2: e={};
consider p be one-to-one FinSequence of I such that
A3: rng p = e and
A4: Product(x,e)=(the multF of L) "**" #(p,x) by Def2;
p={} by A3,A2;
then #(p,x)={} & the multF of L is having_a_unity &
len #(p,x) =0;
then Product(x,e)=the_unity_wrt the multF of L by A4,FINSOP_1:def 1;
hence Product(x,e)=1_L by GROUP_1:22;
end;
now
let e,f be Element of Fin I;
assume
A5: e misses f;
consider pe be one-to-one FinSequence of I such that
A6: rng pe = e and
A7: Product(x,e)=(the multF of L) "**" #(pe,x) by Def2;
consider pf be one-to-one FinSequence of I such that
A8: rng pf = f and
A9: Product(x,f)=(the multF of L) "**" #(pf,x) by Def2;
reconsider pepf=pe^pf as one-to-one FinSequence of I
by A5,A6,A8,FINSEQ_3:91;
A10: #(pepf,x)=#(pe,x)^#(pf,x) by Th3;
rng pepf=e\/f by A6,A8,FINSEQ_1:31; then
Product(x,e\/f)=(the multF of L) "**" #(pepf,x) by Def2;
hence Product(x,e\/f)=Product(x,e) * Product(x,f)
by A7,A9,A10,FINSOP_1:5;
end;
hence thesis by A1;
end;
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
for j being Element of Fin I holds it.j=Product(x,j);
existence
proof
deffunc F(Element of Fin I)=Product(x,$1);
consider f be Function of Fin I,the carrier of L such that
A1: for t be Element of Fin I holds f.t=F(t) from FUNCT_2:sch 4;
the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then [#]OrderedFIN I= Fin I by STRUCT_0:def 3;
then reconsider f as Function of [#]OrderedFIN I, the carrier of L;
for j be Element of Fin I holds f.j=Product(x,j) by A1;
hence thesis;
end;
uniqueness
proof
deffunc F(Element of Fin I)=Product(x,$1);
A2: for a,b being Function of Fin I,the carrier of L st (for q being
Element of Fin I holds a.q=F(q)) & (for q being Element of Fin I holds b.
q=F(q)) holds a=b from BINOP_2:sch 1;
let f,g be Function of [#]OrderedFIN I,the carrier of L;
assume that
A3: for j be Element of Fin I holds f.j=Product(x,j) and
A4: for j be Element of Fin I holds g.j=Product(x,j);
the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then [#]OrderedFIN I= Fin I by STRUCT_0:def 3;
then reconsider f,g as Function of Fin I,the carrier of L;
f=g by A2,A3,A4;
hence thesis;
end;
end;
theorem
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 by Th11;
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
:Def3:
ex p being one-to-one FinSequence of I st rng p = J &
it = (the addF of L) "**" #(p,x);
existence
proof
consider p be FinSequence of I such that
A1: rng p = J & p is one-to-one by Th1;
(the addF of L) "**" #(p,x) is Element of L;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Element of L such that
A2: ex p1 be one-to-one FinSequence of I st rng p1 = J &
X1 = (the addF of L) "**" #(p1,x) and
A3: ex p2 be one-to-one FinSequence of I st rng p2 = J &
X2 = (the addF of L) "**" #(p2,x);
consider p1 be one-to-one FinSequence of I such that
A4: rng p1 = J and
A5: X1 = (the addF of L) "**" #(p1,x) by A2;
consider p2 be one-to-one FinSequence of I such that
A6: rng p2 = J and
A7: X2 = (the addF of L) "**" #(p2,x) by A3;
consider P be Permutation of dom p1 such that
A8: p2=P*p1 & dom P=dom p1 & rng P=dom p1 by A4,A6,BHSP_5:1;
P is Permutation of dom #(p1,x)
proof
dom x =I by PARTFUN1:def 2;
then rng p1 c= dom x by FINSEQ_1:def 4;
then dom (p1 * x)=dom p1 by RELAT_1:27;
hence thesis;
end;
then reconsider P as Permutation of dom #(p1,x);
A9: #(p2,x) = P * #(p1,x)
proof
now
hereby
let t be object;
assume
A10: t in #(p2,x);
consider a,b be object such that
A11: t=[a,b] by A10,RELAT_1:def 1;
consider z be object such that
A12: [a,z] in p2 and
A13: [z,b] in x by A10,A11,RELAT_1:def 8;
consider y be object such that
A14: [a,y] in P and
A15: [y,z] in p1 by A12,A8,RELAT_1:def 8;
[a,y] in P & [y,b] in p1 * x by A14,A13,A15,RELAT_1:def 8;
hence t in P * #(p1,x) by A11,RELAT_1:def 8;
end;
let t be object;
assume
A16: t in P* #(p1,x);
then consider a,b be object such that
A17: t=[a,b] by RELAT_1:def 1;
consider c be object such that
A18: [a,c] in P and
A19: [c,b] in p1*x by A16,A17,RELAT_1:def 8;
consider d be object such that
A20: [c,d] in p1 and
A21: [d,b] in x by A19,RELAT_1:def 8;
[a,d] in p2 by A8,RELAT_1:def 8,A18,A20;
hence t in #(p2,x) by A17,A21,RELAT_1:def 8;
end;
hence thesis;
end;
the addF of L is commutative by GROUP_1A:203;
hence thesis by A9,A5,A7,FINSOP_1:7;
end;
end;
theorem Th12:
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
proof
let I be set,G be TopaddGroup,
f be Function of [#]OrderedFIN I,the carrier of G,
x be Point of G,
B be basis of BOOL2F NeighborhoodSystem x;
[#]OrderedFIN I is directed by Th4;
hence thesis by CARDFIL2:84;
end;
theorem
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)
proof
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;
A1: now
let e be Element of Fin I;
assume
A2: e={};
consider p be one-to-one FinSequence of I such that
A3: rng p = e and
A4: Sum(x,e)=(the addF of L) "**" #(p,x) by Def3;
p={} by A3,A2;
then #(p,x)={} & the addF of L is having_a_unity &
len #(p,x) =0;
then Sum(x,e)=the_unity_wrt the addF of L by A4,FINSOP_1:def 1;
hence Sum(x,e)=0_L by GROUP_1A:21;
end;
now
let e,f be Element of Fin I;
assume
A5: e misses f;
consider pe be one-to-one FinSequence of I such that
A6: rng pe = e and
A7: Sum(x,e)=(the addF of L) "**" #(pe,x) by Def3;
consider pf be one-to-one FinSequence of I such that
A8: rng pf = f and
A9: Sum(x,f)=(the addF of L) "**" #(pf,x) by Def3;
reconsider pepf=pe^pf as one-to-one FinSequence of I
by A5,A6,A8,FINSEQ_3:91;
A10: #(pepf,x)=#(pe,x)^#(pf,x) by Th3;
rng pepf=e\/f by A6,A8,FINSEQ_1:31;
then
Sum(x,e\/f)=(the addF of L) "**" #(pepf,x) by Def3;
hence Sum(x,e\/f)=Sum(x,e) + Sum(x,f) by A7,A9,A10,FINSOP_1:5;
end;
hence thesis by A1;
end;
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
for j being Element of Fin I holds it.j=Sum(x,j);
existence
proof
deffunc F(Element of Fin I)=Sum(x,$1);
consider f be Function of Fin I,the carrier of L such that
A1: for t be Element of Fin I holds f.t=F(t)
from FUNCT_2:sch 4;
the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then
[#]OrderedFIN I= Fin I by STRUCT_0:def 3;
then reconsider f as Function of [#]OrderedFIN I, the carrier of L;
for j be Element of Fin I holds f.j=Sum(x,j) by A1;
hence thesis;
end;
uniqueness
proof
deffunc F(Element of Fin I)=Sum(x,$1);
A2: for a,b being Function of Fin I,the carrier of L st (for q being
Element of Fin I holds a.q=F(q)) & (for q being Element of Fin I holds b.
q=F(q)) holds a=b from BINOP_2:sch 1;
let f,g be Function of [#]OrderedFIN I,the carrier of L;
assume that
A3: for j be Element of Fin I holds f.j=Sum(x,j) and
A4: for j be Element of Fin I holds g.j=Sum(x,j);
the carrier of OrderedFIN I= Fin I by YELLOW_1:1;
then [#]OrderedFIN I= Fin I by STRUCT_0:def 3;
then reconsider f,g as Function of Fin I,the carrier of L;
f=g by A2,A3,A4;
hence thesis;
end;
end;
theorem
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
by Th12;