Copyright (c) 1991 Association of Mizar Users
environ
vocabulary BHSP_1, PRE_TOPC, NORMSP_1, RLVECT_1, SEQ_2, METRIC_1, FUNCT_1,
SEQM_3, ARYTM_3, ARYTM_1, ABSVALUE, RELAT_1, ORDINAL2, SEQ_1, BOOLE,
ARYTM;
notation TARSKI, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, SEQ_1, SEQ_2,
RELAT_1, ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, BHSP_1, NORMSP_1;
constructors REAL_1, NAT_1, SEQ_2, ABSVALUE, BHSP_1, MEMBERED, XBOOLE_0;
clusters STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
theorems TARSKI, REAL_1, NAT_1, AXIOMS, FUNCT_1, SEQ_2, ABSVALUE, SUBSET_1,
RLVECT_1, BHSP_1, NORMSP_1, FUNCT_2, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1;
schemes SEQ_1, FRAENKEL;
begin
reserve X for RealUnitarySpace;
reserve x, y, z, g, g1, g2 for Point of X;
reserve a, q, r for Real;
reserve seq, seq1, seq2, seq' for sequence of X;
reserve k, n, m, m1, m2 for Nat;
deffunc 0'(RealUnitarySpace) = 0. $1;
definition let X, seq;
attr seq is convergent means :Def1:
ex g st for r st r > 0 ex m st for n st n >= m holds dist(seq.n, g) < r;
end;
theorem Th1:
seq is constant implies seq is convergent
proof
assume seq is constant;
then consider x such that
A1: for n holds seq.n = x by NORMSP_1:def 4;
take g = x;
let r such that
A2: r > 0;
take m = 0;
let n such that n >= m;
dist((seq.n) , g) = dist(x , g) by A1
.= 0 by BHSP_1:41;
hence dist((seq.n) , g) < r by A2;
end;
theorem Th2:
seq is convergent & (ex k st for n st k <= n holds seq'.n = seq.n)
implies seq' is convergent
proof
assume that
A1: seq is convergent and
A2: ex k st for n st k <= n holds seq'.n = seq.n;
consider g such that
A3: for r st r > 0 ex m st for n st n >= m holds
dist((seq.n) , g) < r by A1,Def1;
consider k such that
A4: for n st n >= k holds seq'.n = seq.n by A2;
take h = g;
let r; assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , h) < r by A3;
A6: now assume
A7: k <= m1;
take m = m1;
let n; assume
A8: n >= m;
then n >= k by A7,AXIOMS:22;
then seq'.n = seq.n by A4;
hence dist((seq'.n) , h) < r by A5,A8;
end;
now assume
A9: m1 <= k;
take m = k;
let n; assume
A10: n >= m;
then n >= m1 by A9,AXIOMS:22;
then dist((seq.n) , g) < r by A5;
hence dist((seq'.n) , h) < r by A4,A10;
end;
hence ex m st for n st n >= m holds
dist((seq'.n) , h) < r by A6;
end;
theorem Th3:
seq1 is convergent & seq2 is convergent implies
seq1 + seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds
dist((seq1.n) , g1) < r by A1,Def1;
consider g2 such that
A4: for r st r > 0 ex m st for n st n >= m holds
dist((seq2.n) , g2) < r by A2,Def1;
take g = g1 + g2;
let r; assume r > 0;
then A5: r/2 > 0 by SEQ_2:3;
then consider m1 such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3;
consider m2 such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: n >= k;
m1 + m2 >= m1 by NAT_1:37;
then n >= m1 by A8,AXIOMS:22;
then A9: dist((seq1.n) , g1) < r/2 by A6;
k >= m2 by NAT_1:37;
then n >= m2 by A8,AXIOMS:22;
then dist((seq2.n) , g2) < r/2 by A7;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2
by A9,REAL_1:67;
then A10: dist((seq1.n) , g1) + dist((seq2.n) , g2) < r by XCMPLX_1:66;
dist((seq1 + seq2).n , g) =
dist((seq1.n) + (seq2.n) , (g1 + g2)) by NORMSP_1:def 5;
then dist((seq1 + seq2).n , g) <= dist((seq1.n) , g1) +
dist((seq2.n) , g2) by BHSP_1:47;
hence dist((seq1 + seq2).n , g) < r by A10,AXIOMS:22;
end;
theorem Th4:
seq1 is convergent & seq2 is convergent implies
seq1 - seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds
dist((seq1.n) , g1) < r by A1,Def1;
consider g2 such that
A4: for r st r > 0 ex m st for n st n >= m holds
dist((seq2.n) , g2) < r by A2,Def1;
take g = g1 - g2;
let r; assume r > 0;
then A5: r/2 > 0 by SEQ_2:3;
then consider m1 such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3;
consider m2 such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: n >= k;
m1 + m2 >= m1 by NAT_1:37;
then n >= m1 by A8,AXIOMS:22;
then A9: dist((seq1.n) , g1) < r/2 by A6;
k >= m2 by NAT_1:37;
then n >= m2 by A8,AXIOMS:22;
then dist((seq2.n) , g2) < r/2 by A7;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2
by A9,REAL_1:67;
then A10: dist((seq1.n) , g1) + dist((seq2.n) , g2) < r by XCMPLX_1:66;
dist((seq1 - seq2).n , g) =
dist((seq1.n) - (seq2.n) , (g1 - g2)) by NORMSP_1:def 6;
then dist((seq1 - seq2).n , g) <= dist((seq1.n) , g1) +
dist((seq2.n) , g2) by BHSP_1:48;
hence dist((seq1 - seq2).n , g) < r by A10,AXIOMS:22;
end;
theorem Th5:
seq is convergent implies a * seq is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n
st n >= m holds dist((seq.n) , g) < r by Def1;
take h = a * g;
A2: now assume
A3: a = 0;
let r; assume r > 0;
then consider m1 such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n; assume n >= k;
then A5: dist((seq.n) , g) < r by A4;
dist(a * (seq.n) , a * g)
= dist(0 * (seq.n) , 0'(X)) by A3,RLVECT_1:23
.= dist(0'(X) , 0'(X)) by RLVECT_1:23
.= 0 by BHSP_1:41;
then dist(a * (seq.n) , h) < r by A5,BHSP_1:44;
hence dist((a * seq).n , h) < r by NORMSP_1:def 8;
end;
now assume
A6: a <> 0;
then A7: abs(a) > 0 by ABSVALUE:6;
let r such that
A8: r > 0;
A9: abs(a) <> 0 by A6,ABSVALUE:6;
0/abs(a) = 0;
then r/abs(a) > 0 by A7,A8,REAL_1:73;
then consider m1 such that
A10: for n st n >= m1 holds dist((seq.n) , g) < r/abs(a) by A1;
take k = m1;
let n; assume n >= k;
then A11: dist((seq.n) , g) < r/abs(a) by A10;
A12: dist(a * (seq.n) , a * g)
= ||.(a * (seq.n)) - (a * g).|| by BHSP_1:def 5
.= ||.a * ((seq.n) - g).|| by RLVECT_1:48
.= abs(a) * ||.(seq.n) - g.|| by BHSP_1:33
.= abs(a) * dist((seq.n) , g) by BHSP_1:def 5;
abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
.= abs(a) *abs(a)" * r by XCMPLX_1:4
.= 1 * r by A9,XCMPLX_0:def 7
.= r;
then dist((a *(seq.n)) , h) < r by A7,A11,A12,REAL_1:70;
hence dist((a * seq).n , h) < r by NORMSP_1:def 8;
end;
hence thesis by A2;
end;
theorem Th6:
seq is convergent implies - seq is convergent
proof
assume seq is convergent;
then (-1) * seq is convergent by Th5;
hence thesis by BHSP_1:77;
end;
theorem Th7:
seq is convergent implies seq + x is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n
st n >= m holds dist((seq.n) , g) < r by Def1;
take g + x;
let r; assume r > 0;
then consider m1 such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n; assume n >= k;
then A3: dist((seq.n) , g) < r by A2;
dist((seq.n) + x , g + x) <= dist((seq.n) , g) +
dist(x , x) by BHSP_1:47;
then dist((seq.n) + x , g + x) <= dist((seq.n) , g) + 0
by BHSP_1:41;
then dist((seq.n) + x , g + x) < r by A3,AXIOMS:22;
hence thesis by BHSP_1:def 12;
end;
theorem Th8:
seq is convergent implies seq - x is convergent
proof
assume seq is convergent;
then seq + (-x) is convergent by Th7;
hence thesis by BHSP_1:78;
end;
theorem Th9:
seq is convergent iff ex g st for r st r > 0 ex m st for n
st n >= m holds ||.(seq.n) - g.|| < r
proof
thus seq is convergent implies ex g st for r st r > 0 ex m st for n
st n >= m holds ||.(seq.n) - g.|| < r
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n
st n >= m holds dist((seq.n) , g) < r by Def1;
take g;
let r; assume r > 0;
then consider m1 such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n; assume n >= k;
then dist((seq.n) , g) < r by A2;
hence thesis by BHSP_1:def 5;
end;
( ex g st for r st r > 0 ex m st for n
st n >= m holds ||.(seq.n) - g.|| < r ) implies seq is convergent
proof
given g such that
A3: for r st r > 0 ex m st for n
st n >= m holds ||.(seq.n) - g.|| < r;
take g;
let r; assume r > 0;
then consider m1 such that
A4: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A3;
take k = m1;
let n; assume n >= k;
then ||.(seq.n) - g.|| < r by A4;
hence thesis by BHSP_1:def 5;
end;
hence thesis;
end;
definition let X, seq;
assume A1: seq is convergent;
func lim seq -> Point of X means :Def2:
for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , it) < r;
existence by A1,Def1;
uniqueness
proof
for x , y st
( for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , x) < r ) &
( for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y) < r )
holds x = y
proof
given x , y such that
A2: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , x) < r and
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y) < r and
A4: x <> y;
A5: dist(x , y) > 0 by A4,BHSP_1:45;
then A6: dist(x , y)/4 > 0/4 by REAL_1:73;
then consider m1 such that
A7: for n st n >= m1 holds dist((seq.n) , x) < dist(x , y)/4 by A2;
consider m2 such that
A8: for n st n >= m2 holds dist((seq.n) , y) < dist(x , y)/4 by A3,A6;
A9: now assume
m1 <= m2;
then A10: dist((seq.m2) , x) < dist(x , y)/4 by A7;
dist((seq.m2) , y) < dist(x , y)/4 by A8;
then dist((seq.m2) , x) + dist((seq.m2) , y) <
dist(x , y)/4 + dist(x , y)/4 by A10,REAL_1:67;
then A11: dist((seq.m2) , x) + dist((seq.m2) , y) <= dist(x , y)/2 by XCMPLX_1:
72;
dist(x , y) = dist(x - (seq.m2) , y - (seq.m2)) by BHSP_1:49;
then dist(x , y) <= dist((seq.m2) , x) + dist((seq.m2) , y) by BHSP_1:50;
then dist(x , y) <= dist(x , y)/2 by A11,AXIOMS:22;
hence contradiction by A5,SEQ_2:4;
end;
now assume
m1 >= m2;
then A12: dist((seq.m1) , y) < dist(x , y)/4 by A8;
dist((seq.m1) , x) < dist(x , y)/4 by A7;
then dist((seq.m1) , x) + dist((seq.m1) , y) < dist(x , y)/4 + dist(x , y)
/4
by A12,REAL_1:67;
then A13: dist((seq.m1) , x) + dist((seq.m1) , y) <= dist(x , y)/2 by XCMPLX_1:
72;
dist(x , y) = dist(x - (seq.m1) , y - (seq.m1)) by BHSP_1:49;
then dist(x , y) <= dist((seq.m1) , x) + dist((seq.m1) , y) by BHSP_1:50;
then dist(x , y) <= dist(x , y)/2 by A13,AXIOMS:22;
hence contradiction by A5,SEQ_2:4;
end;
hence contradiction by A9;
end;
hence thesis;
end;
end;
theorem Th10:
seq is constant & x in rng seq implies lim seq = x
proof
assume that
A1: seq is constant and
A2: x in rng seq;
consider y such that
A3: rng seq = {y} by A1,NORMSP_1:27;
consider z such that
A4: for n holds seq.n = z by A1,NORMSP_1:def 4;
A5: x = y by A2,A3,TARSKI:def 1;
A6: seq is convergent by A1,Th1;
now let r such that
A7: r > 0;
take m = 0;
let n such that n >= m;
n in NAT;
then n in dom seq by NORMSP_1:17;
then seq.n in rng seq by FUNCT_1:def 5;
then z in rng seq by A4;
then z = x by A3,A5,TARSKI:def 1;
then seq.n = x by A4;
hence dist((seq.n) , x) < r by A7,BHSP_1:41;
end;
hence lim seq = x by A6,Def2;
end;
theorem
seq is constant & (ex n st seq.n = x) implies lim seq = x
proof
assume that
A1: seq is constant and
A2: ex n st seq.n = x;
consider n such that
A3: seq.n = x by A2;
n in NAT;
then n in dom seq by NORMSP_1:17;
then x in rng seq by A3,FUNCT_1:def 5;
hence lim seq = x by A1,Th10;
end;
theorem
seq is convergent & (ex k st for n st n >= k holds seq'.n = seq.n)
implies lim seq = lim seq'
proof
assume that
A1: seq is convergent and
A2: ex k st for n st n >= k holds seq'.n = seq.n;
A3: seq' is convergent by A1,A2,Th2;
consider k such that
A4: for n st n >= k holds seq'.n = seq.n by A2;
now let r; assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , (lim seq)) < r by A1,Def2;
A6: now assume
A7: k <= m1;
take m = m1;
let n; assume
A8: n >= m;
then n >= k by A7,AXIOMS:22;
then seq'.n = seq.n by A4;
hence dist((seq'.n) , (lim seq)) < r by A5,A8;
end;
now assume
A9: m1 <= k;
take m = k;
let n; assume
A10: n >= m;
then n >= m1 by A9,AXIOMS:22;
then dist((seq.n) , (lim seq)) < r by A5;
hence dist((seq'.n) , (lim seq)) < r by A4,A10;
end;
hence ex m st for n st n >= m holds
dist((seq'.n) , (lim seq)) < r by A6;
end;
hence thesis by A3,Def2;
end;
theorem Th13:
seq1 is convergent & seq2 is convergent implies
lim (seq1 + seq2) = (lim seq1) + (lim seq2)
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
A3: seq1 + seq2 is convergent by A1,A2,Th3;
set g1 = lim seq1;
set g2 = lim seq2;
set g = g1 + g2;
now let r; assume r > 0;
then A4: r/2 > 0 by SEQ_2:3;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
consider m2 such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
take k = m1 + m2;
let n such that
A7: n >= k;
m1 + m2 >= m1 by NAT_1:37;
then n >= m1 by A7,AXIOMS:22;
then A8: dist((seq1.n) , g1) < r/2 by A5;
k >= m2 by NAT_1:37;
then n >= m2 by A7,AXIOMS:22;
then dist((seq2.n) , g2) < r/2 by A6;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2
by A8,REAL_1:67;
then A9: dist((seq1.n) , g1) + dist((seq2.n) , g2) < r by XCMPLX_1:66;
dist((seq1 + seq2).n , g)
= dist((seq1.n) + (seq2.n) , g1 + g2) by NORMSP_1:def 5;
then dist((seq1 + seq2).n , g)
<= dist((seq1.n) , g1) + dist((seq2.n) , g2) by BHSP_1:47;
hence dist((seq1 + seq2).n , g) < r by A9,AXIOMS:22;
end;
hence thesis by A3,Def2;
end;
theorem Th14:
seq1 is convergent & seq2 is convergent implies
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
A3: seq1 - seq2 is convergent by A1,A2,Th4;
set g1 = lim seq1;
set g2 = lim seq2;
set g = g1 - g2;
now let r; assume r > 0;
then A4: r/2 > 0 by SEQ_2:3;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
consider m2 such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
take k = m1 + m2;
let n such that
A7: n >= k;
m1 + m2 >= m1 by NAT_1:37;
then n >= m1 by A7,AXIOMS:22;
then A8: dist((seq1.n) , g1) < r/2 by A5;
k >= m2 by NAT_1:37;
then n >= m2 by A7,AXIOMS:22;
then dist((seq2.n) , g2) < r/2 by A6;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2
by A8,REAL_1:67;
then A9: dist((seq1.n) , g1) + dist((seq2.n) , g2) < r by XCMPLX_1:66;
dist((seq1 - seq2).n , g)
= dist((seq1.n) - (seq2.n) , g1 - g2) by NORMSP_1:def 6;
then dist((seq1 - seq2).n , g)
<= dist((seq1.n) , g1) + dist((seq2.n) , g2) by BHSP_1:48;
hence dist((seq1 - seq2).n , g) < r by A9,AXIOMS:22;
end;
hence thesis by A3,Def2;
end;
theorem Th15:
seq is convergent implies lim (a * seq) = a * (lim seq)
proof
assume
A1: seq is convergent;
then A2: a * seq is convergent by Th5;
set g = lim seq;
set h = a * g;
A3: now assume
A4: a = 0;
let r; assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
take k = m1;
let n; assume n >= k;
then A6: dist((seq.n) , g) < r by A5;
dist(a * (seq.n) , a * g) =
dist(0 * (seq.n) , 0'(X)) by A4,RLVECT_1:23
.= dist(0'(X) , 0'(X)) by RLVECT_1:23
.= 0 by BHSP_1:41;
then dist(a * (seq.n) , h) < r by A6,BHSP_1:44;
hence dist((a * seq).n , h) < r by NORMSP_1:def 8;
end;
now assume
A7: a <> 0;
then A8: abs(a) > 0 by ABSVALUE:6;
let r such that
A9: r > 0;
A10: abs(a) <> 0 by A7,ABSVALUE:6;
0/abs(a) =0;
then r/abs(a) > 0 by A8,A9,REAL_1:73;
then consider m1 such that
A11: for n st n >= m1 holds
dist((seq.n) , g) < r/abs(a) by A1,Def2;
take k = m1;
let n; assume
n >= k;
then A12: dist((seq.n) , g) < r/abs(a) by A11;
A13: dist(a * (seq.n) , a * g)
= ||.(a * (seq.n)) - (a * g).|| by BHSP_1:def 5
.= ||.a * ((seq.n) - g).|| by RLVECT_1:48
.= abs(a) * ||.(seq.n) - g.|| by BHSP_1:33
.= abs(a) * dist((seq.n) , g) by BHSP_1:def 5;
abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
.= abs(a) *abs(a)" * r by XCMPLX_1:4
.= 1 * r by A10,XCMPLX_0:def 7
.= r;
then dist(a * (seq.n) , h) < r by A8,A12,A13,REAL_1:70;
hence dist((a * seq).n , h) < r by NORMSP_1:def 8;
end;
hence thesis by A2,A3,Def2;
end;
theorem Th16:
seq is convergent implies lim (- seq) = - (lim seq)
proof
assume
seq is convergent;
then lim ((-1) * seq) = (-1) * (lim seq) by Th15;
then lim (- seq) = (-1) * (lim seq) by BHSP_1:77;
hence thesis by RLVECT_1:29;
end;
theorem Th17:
seq is convergent implies lim (seq + x) = (lim seq) + x
proof
assume
A1: seq is convergent;
then A2: seq + x is convergent by Th7;
set g = lim seq;
now let r; assume
r > 0;
then consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
take k = m1;
let n; assume n >= k;
then A4: dist((seq.n) , g) < r by A3;
dist((seq.n) , g)
= dist((seq.n) - (-x) , g - (-x)) by BHSP_1:49
.= dist((seq.n) + (-(-x)) , g - (-x)) by RLVECT_1:def 11
.= dist((seq.n) + x , g - (-x)) by RLVECT_1:30
.= dist((seq.n) + x , g + (-(-x))) by RLVECT_1:def 11
.= dist((seq.n) + x , g + x) by RLVECT_1:30;
hence dist((seq + x).n , (g + x)) < r by A4,BHSP_1:def 12;
end;
hence thesis by A2,Def2;
end;
theorem
seq is convergent implies lim (seq - x) = (lim seq) - x
proof
assume
seq is convergent;
then lim (seq + (-x)) = (lim seq) + (-x) by Th17;
then lim (seq - x) = (lim seq) + (-x) by BHSP_1:78;
hence thesis by RLVECT_1:def 11;
end;
theorem Th19:
seq is convergent implies
( lim seq = g iff for r st r > 0 ex m st for n st n >= m
holds ||.(seq.n) - g.|| < r )
proof
assume
A1: seq is convergent;
thus
lim seq = g implies ( for r st r > 0 ex m st for n st n >= m
holds ||.(seq.n) - g.|| < r )
proof
assume
A2: lim seq = g;
let r; assume r > 0;
then consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
take k = m1;
let n; assume n >= k;
then dist((seq.n) , g) < r by A3;
hence thesis by BHSP_1:def 5;
end;
( for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r )
implies lim seq = g
proof
assume
A4: ( for r st r > 0 ex m st for n st n >= m
holds ||.(seq.n) - g.|| < r );
now let r; assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A4;
take k = m1;
let n; assume
n >= k;
then ||.(seq.n) - g.|| < r by A5;
hence dist((seq.n) , g) < r by BHSP_1:def 5;
end;
hence thesis by A1,Def2;
end;
hence thesis;
end;
definition let X, seq;
func ||.seq.|| -> Real_Sequence means
:Def3: for n holds it.n =||.(seq.n).||;
existence
proof
deffunc _F(Nat) = ||.(seq.$1).||;
consider s being Real_Sequence such that
A1: for n holds s.n = _F(n) from ExRealSeq;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume
A2: ( for n holds s.n = ||.(seq.n).|| ) &
( for n holds t.n = ||.(seq.n).|| );
now let n;
s.n = ||.(seq.n).|| by A2; hence
s.n = t.n by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
theorem Th20:
seq is convergent implies ||.seq.|| is convergent
proof
assume
seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n
st n >= m holds ||.(seq.n) - g.|| < r by Th9;
now let r be real number;
A2: r is Real by XREAL_0:def 1;
assume r > 0;
then consider m1 such that
A3: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2;
take k = m1;
now let n; assume
n >= k;
then A4: ||.(seq.n) - g.|| < r by A3;
abs(||.(seq.n).|| - ||.g.||) <= ||.(seq.n) - g.|| by BHSP_1:39;
then abs(||.(seq.n).|| - ||.g.||) < r by A4,AXIOMS:22;
hence abs(||.seq.||.n - ||.g.||) < r by Def3;
end;
hence for n st k <= n holds abs(||.seq.||.n - ||.g.||) < r;
end;
hence thesis by SEQ_2:def 6;
end;
theorem Th21:
seq is convergent & lim seq = g implies
||.seq.|| is convergent & lim ||.seq.|| = ||.g.||
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: ||.seq.|| is convergent by A1,Th20;
now let r be real number;
A4: r is Real by XREAL_0:def 1;
assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r
by A1,A2,A4,Th19;
take k = m1;
now let n; assume n >= k;
then A6: ||.(seq.n) - g.|| < r by A5;
abs(||.(seq.n).|| - ||.g.||) <= ||.(seq.n) - g.||
by BHSP_1:39;
then abs(||.(seq.n).|| - ||.g.||) < r by A6,AXIOMS:22;
hence abs(||.seq.||.n - ||.g.||) < r by Def3;
end;
hence for n st k <= n holds abs(||.seq.||.n - ||.g.||) < r;
end;
hence thesis by A3,SEQ_2:def 7;
end;
theorem Th22:
seq is convergent & lim seq = g implies
( ||.seq - g.|| is convergent & lim ||.seq - g.|| = 0 )
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
seq - g is convergent by A1,Th8;
then A3: ||.seq - g.|| is convergent by Th20;
now let r be real number;
A4: r is Real by XREAL_0:def 1;
assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
take k = m1;
let n; assume
n >= k;
then ||.(seq.n) - g.|| < r by A5;
then A6: ||.((seq.n) - g ) - 0'(X).|| < r by RLVECT_1:26;
abs(||.(seq.n) - g.|| - ||.0'(X).||) <= ||.((seq.n) - g ) - 0'(X)
.||
by BHSP_1:39;
then abs(||.(seq.n) - g.|| - ||.0'(X).||) < r by A6,AXIOMS:22;
then abs((||.(seq.n) - g.|| - 0)) < r by BHSP_1:32;
then abs((||.(seq - g).n.|| - 0)) < r by NORMSP_1:def 7;
hence abs((||.seq - g.||.n - 0)) < r by Def3;
end;
hence thesis by A3,SEQ_2:def 7;
end;
definition
let X;
let seq;
let x;
func dist(seq , x) -> Real_Sequence means
:Def4: for n holds it.n =dist((seq.n) , x);
existence
proof
deffunc _F(Nat) = dist((seq.$1) , x);
consider s being Real_Sequence such that
A1: for n holds s.n = _F(n) from ExRealSeq;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume
A2: ( for n holds s.n = dist((seq.n) , x) ) &
( for n holds t.n = dist((seq.n) , x) );
now let n;
s.n = dist((seq.n) , x) by A2; hence
s.n = t.n by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
theorem Th23:
( seq is convergent & lim seq = g ) implies
dist(seq , g) is convergent
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
now let r be real number;
A3: r is Real by XREAL_0:def 1;
assume r > 0;
then consider m1 such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,A3,Def2;
take k = m1;
now let n; assume
n >= k;
then A5: dist((seq.n) , g) < r by A4;
dist((seq.n) , g) >= 0 by BHSP_1:44;
then abs((dist((seq.n) , g) - 0))
= dist((seq.n) , g) by ABSVALUE:def 1;
hence abs((dist(seq , g).n - 0)) < r by A5,Def4;
end;
hence for n st k <= n holds abs((dist(seq , g).n - 0)) < r;
end;
hence thesis by SEQ_2:def 6;
end;
theorem Th24:
seq is convergent & lim seq = g implies
( dist(seq , g) is convergent & lim dist(seq , g) = 0 )
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: dist(seq , g) is convergent by A1,A2,Th23;
now let r be real number;
A4: r is Real by XREAL_0:def 1;
assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,A4,Def2;
take k = m1;
let n; assume
n >= k;
then A6: dist((seq.n) , g) < r by A5;
dist((seq.n) , g) >= 0 by BHSP_1:44;
then abs((dist((seq.n) , g) - 0))
= dist((seq.n) , g) by ABSVALUE:def 1;
hence abs((dist(seq , g).n - 0)) < r by A6,Def4;
end;
hence thesis by A3,SEQ_2:def 7;
end;
theorem
seq1 is convergent & lim seq1 = g1 &
seq2 is convergent & lim seq2 = g2 implies
||.seq1 + seq2.|| is convergent &
lim ||.seq1 + seq2.|| = ||.g1 + g2.||
proof
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2;
A5: seq1 + seq2 is convergent by A1,A3,Th3;
lim (seq1 + seq2) = g1 + g2 by A1,A2,A3,A4,Th13;
hence thesis by A5,Th21;
end;
theorem
seq1 is convergent & lim seq1 = g1 &
seq2 is convergent & lim seq2 = g2 implies
||.(seq1 + seq2) - (g1 + g2).|| is convergent
& lim ||.(seq1 + seq2) - (g1 + g2).|| = 0
proof
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2;
A5: seq1 + seq2 is convergent by A1,A3,Th3;
lim (seq1 + seq2) = g1 + g2 by A1,A2,A3,A4,Th13;
hence thesis by A5,Th22;
end;
theorem
seq1 is convergent & lim seq1 = g1 &
seq2 is convergent & lim seq2 = g2 implies
||.seq1 - seq2.|| is convergent &
lim ||.seq1 - seq2.|| = ||.g1 - g2.||
proof
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2;
A5: seq1 - seq2 is convergent by A1,A3,Th4;
lim (seq1 - seq2) = g1 - g2 by A1,A2,A3,A4,Th14;
hence thesis by A5,Th21;
end;
theorem
seq1 is convergent & lim seq1 = g1 &
seq2 is convergent & lim seq2 = g2 implies
||.(seq1 - seq2) - (g1 - g2).|| is convergent
& lim ||.(seq1 - seq2) - (g1 - g2).|| = 0
proof
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2;
A5: seq1 - seq2 is convergent by A1,A3,Th4;
lim (seq1 - seq2) = g1 - g2 by A1,A2,A3,A4,Th14;
hence thesis by A5,Th22;
end;
theorem
seq is convergent & lim seq = g implies
||.a * seq.|| is convergent &
lim ||.a * seq.|| = ||.a * g.||
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: a * seq is convergent by A1,Th5;
lim (a * seq) = a * g by A1,A2,Th15;
hence thesis by A3,Th21;
end;
theorem
seq is convergent & lim seq = g implies
||.(a * seq) - (a * g).|| is convergent
& lim ||.(a * seq) - (a * g).|| = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: a * seq is convergent by A1,Th5;
lim (a * seq) = a * g by A1,A2,Th15;
hence thesis by A3,Th22;
end;
theorem
seq is convergent & lim seq = g implies
||.- seq.|| is convergent &
lim ||.- seq.|| = ||.- g.||
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: - seq is convergent by A1,Th6;
lim (- seq) = - g by A1,A2,Th16;
hence thesis by A3,Th21;
end;
theorem
seq is convergent & lim seq = g implies
||.(- seq) - (- g).|| is convergent
& lim ||.(- seq) - (- g).|| = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: - seq is convergent by A1,Th6;
lim (- seq) = - g by A1,A2,Th16;
hence thesis by A3,Th22;
end;
Lm1:
seq is convergent & lim seq = g implies
||.seq + x.|| is convergent &
lim ||.seq + x.|| = ||.g + x.||
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: seq + x is convergent by A1,Th7;
lim (seq + x) = g + x by A1,A2,Th17;
hence thesis by A3,Th21;
end;
theorem Th33:
seq is convergent & lim seq = g implies
||.(seq + x) - (g + x).|| is convergent
& lim ||.(seq + x) - (g + x).|| = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: seq + x is convergent by A1,Th7;
lim (seq + x) = g + x by A1,A2,Th17;
hence thesis by A3,Th22;
end;
theorem
seq is convergent & lim seq = g implies
||.seq - x.|| is convergent &
lim ||.seq - x.|| = ||.g - x.||
proof
assume seq is convergent & lim seq = g;
then ||.seq + (-x).|| is convergent &
lim ||.seq + (-x).|| = ||.g + (-x).|| by Lm1;
then ||.seq - x.|| is convergent &
lim ||.seq - x.|| = ||.g + (-x).|| by BHSP_1:78;
hence thesis by RLVECT_1:def 11;
end;
theorem
seq is convergent & lim seq = g implies
||.(seq - x) - (g - x).|| is convergent
& lim ||.(seq - x) - (g - x).|| = 0
proof
assume seq is convergent & lim seq = g;
then ||.(seq + (-x)) - (g + (-x)).|| is convergent &
lim ||.(seq + (-x)) - (g + (-x)).|| = 0 by Th33;
then ||.(seq - x) - (g + (-x)).|| is convergent &
lim ||.(seq - x) - (g + (-x)).|| = 0 by BHSP_1:78;
hence thesis by RLVECT_1:def 11;
end;
theorem
seq1 is convergent & lim seq1 = g1 &
seq2 is convergent & lim seq2 = g2 implies
dist((seq1 + seq2) , (g1 + g2)) is convergent &
lim dist((seq1 + seq2) , (g1 + g2)) = 0
proof
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2;
A5: seq1 + seq2 is convergent by A1,A3,Th3;
lim (seq1 + seq2) = g1 + g2 by A1,A2,A3,A4,Th13;
hence thesis by A5,Th24;
end;
theorem
seq1 is convergent & lim seq1 = g1 &
seq2 is convergent & lim seq2 = g2 implies
dist((seq1 - seq2) , (g1 - g2)) is convergent &
lim dist((seq1 - seq2) , (g1 - g2)) = 0
proof
assume that
A1: seq1 is convergent and
A2: lim seq1 = g1 and
A3: seq2 is convergent and
A4: lim seq2 = g2;
A5: seq1 - seq2 is convergent by A1,A3,Th4;
lim (seq1 - seq2) = g1 - g2 by A1,A2,A3,A4,Th14;
hence thesis by A5,Th24;
end;
theorem
seq is convergent & lim seq = g implies
dist((a * seq) , (a * g)) is convergent &
lim dist((a * seq) , (a * g)) = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: a * seq is convergent by A1,Th5;
lim (a * seq) = a * g by A1,A2,Th15;
hence thesis by A3,Th24;
end;
theorem
seq is convergent & lim seq = g implies
dist((seq + x) , (g + x)) is convergent &
lim dist((seq + x) , (g + x)) = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: seq + x is convergent by A1,Th7;
lim (seq + x) = g + x by A1,A2,Th17;
hence thesis by A3,Th24;
end;
definition let X, x, r;
func Ball(x,r) -> Subset of X equals
:Def5: {y where y is Point of X : ||.x - y.|| < r};
coherence
proof defpred _P[Point of X] means ||.x - $1.|| < r;
{y where y is Point of X : _P[y]} c= the carrier of X from Fr_Set0;
hence thesis;
end;
func cl_Ball(x,r) -> Subset of X equals
:Def6: {y where y is Point of X : ||.x - y.|| <= r};
coherence
proof defpred _P[Point of X] means ||.x - $1.|| <= r;
{y where y is Point of X : _P[y]} c= the carrier of X from Fr_Set0;
hence thesis;
end;
func Sphere(x,r) -> Subset of X equals
:Def7: {y where y is Point of X : ||.x - y.|| = r};
coherence
proof defpred _P[Point of X] means ||.x - $1.|| = r;
{y where y is Point of X : _P[y]} c= the carrier of X from Fr_Set0;
hence thesis;
end;
end;
theorem Th40:
z in Ball(x,r) iff ||.x - z.|| < r
proof
thus z in Ball(x,r) implies ||.x - z.|| < r
proof
assume
z in Ball(x,r);
then z in { y where y is Point of X : ||.x - y.|| < r} by Def5;
then ex y be Point of X st z = y & ||.x - y.|| < r;
hence ||.x - z.|| < r;
end;
||.x - z.|| < r implies z in Ball(x,r)
proof
assume
||.x - z.|| < r;
then z in {y where y is Point of X : ||.x - y.|| < r};
hence z in Ball(x,r) by Def5;
end;
hence thesis;
end;
theorem Th41:
z in Ball(x,r) iff dist(x,z) < r
proof
thus z in Ball(x,r) implies dist(x,z) < r
proof
assume z in Ball(x,r);
then ||.x - z.|| < r by Th40;
hence thesis by BHSP_1:def 5;
end;
assume dist(x,z) < r;
then ||.x - z.|| < r by BHSP_1:def 5;
hence z in Ball(x,r) by Th40;
end;
theorem
r > 0 implies x in Ball(x,r)
proof
assume A1: r > 0;
dist(x,x) = 0 by BHSP_1:41;
hence thesis by A1,Th41;
end;
theorem
y in Ball(x,r) & z in Ball(x,r) implies dist(y,z) < 2 * r
proof
assume that
A1: y in Ball(x,r) and
A2: z in Ball(x,r);
A3: dist(x,y) < r by A1,Th41;
A4: dist(x,z) < r by A2,Th41;
A5: dist(x,y) + dist(x,z) < r + dist(x,z) by A3,REAL_1:53;
r + dist(x,z) < r + r by A4,REAL_1:53;
then r + dist(x,z) < 2 * r by XCMPLX_1:11;
then A6: dist(x,y) + dist(x,z) < 2 * r by A5,AXIOMS:22;
dist(y,z) <= dist(y,x) + dist(x,z) by BHSP_1:42;
hence thesis by A6,AXIOMS:22;
end;
theorem
y in Ball(x,r) implies y - z in Ball(x - z,r)
proof
assume y in Ball(x,r);
then A1: dist(x,y) < r by Th41;
dist(x - z,y - z) = dist(x,y) by BHSP_1:49;
hence thesis by A1,Th41;
end;
theorem
y in Ball(x,r) implies (y - x) in Ball (0.(X),r)
proof
assume y in Ball(x,r);
then ||.x - y.|| < r by Th40;
then ||.(-y) + x.|| < r by RLVECT_1:def 11;
then ||.-(y - x).|| < r by RLVECT_1:47;
then ||.0'(X) - (y - x).|| < r by RLVECT_1:27;
hence thesis by Th40;
end;
theorem
y in Ball(x,r) & r <= q implies y in Ball(x,q)
proof
assume that
A1: y in Ball(x,r) and
A2: r <= q;
||.x - y.|| < r by A1,Th40;
then ||.x - y.|| < q by A2,AXIOMS:22;
hence thesis by Th40;
end;
theorem Th47:
z in cl_Ball(x,r) iff ||.x - z.|| <= r
proof
thus z in cl_Ball(x,r) implies ||.x - z.|| <= r
proof
assume
z in cl_Ball(x,r);
then z in { y where y is Point of X : ||.x - y.|| <= r} by Def6;
then ex y be Point of X st z = y & ||.x - y.|| <= r;
hence ||.x - z.|| <= r;
end;
assume ||.x - z.|| <= r;
then z in {y where y is Point of X : ||.x - y.|| <= r};
hence z in cl_Ball(x,r) by Def6;
end;
theorem Th48:
z in cl_Ball(x,r) iff dist(x,z) <= r
proof
thus z in cl_Ball(x,r) implies dist(x,z) <= r
proof
assume
z in cl_Ball(x,r);
then ||.x - z.|| <= r by Th47;
hence thesis by BHSP_1:def 5;
end;
assume dist(x,z) <= r;
then ||.x - z.|| <= r by BHSP_1:def 5;
hence z in cl_Ball(x,r) by Th47;
end;
theorem
r >= 0 implies x in cl_Ball(x,r)
proof
assume r >= 0;
then dist(x,x) <= r by BHSP_1:41;
hence thesis by Th48;
end;
theorem Th50:
y in Ball(x,r) implies y in cl_Ball(x,r)
proof
assume y in Ball(x,r);
then ||.x - y.|| <= r by Th40;
hence thesis by Th47;
end;
theorem Th51:
z in Sphere(x,r) iff ||.x - z.|| = r
proof
thus z in Sphere(x,r) implies ||.x - z.|| = r
proof
assume z in Sphere(x,r);
then z in { y where y is Point of X : ||.x - y.|| = r} by Def7;
then ex y be Point of X st z = y & ||.x - y.|| = r;
hence ||.x - z.|| = r;
end;
assume ||.x - z.|| = r;
then z in {y where y is Point of X : ||.x - y.|| = r};
hence z in Sphere(x,r) by Def7;
end;
theorem
z in Sphere(x,r) iff dist(x,z) = r
proof
thus z in Sphere(x,r) implies dist(x,z) = r
proof
assume
z in Sphere(x,r);
then ||.x - z.|| = r by Th51;
hence thesis by BHSP_1:def 5;
end;
assume dist(x,z) = r;
then ||.x - z.|| = r by BHSP_1:def 5;
hence z in Sphere(x,r) by Th51;
end;
theorem
y in Sphere(x,r) implies y in cl_Ball(x,r)
proof
assume y in Sphere(x,r);
then ||.x - y.|| = r by Th51;
hence thesis by Th47;
end;
theorem Th54:
Ball(x,r) c= cl_Ball(x,r)
proof
for y holds y in Ball(x,r) implies y in cl_Ball(x,r) by Th50;
hence thesis by SUBSET_1:7;
end;
theorem Th55:
Sphere(x,r) c= cl_Ball(x,r)
proof
now let y; assume y in Sphere(x,r);
then ||.x - y.|| = r by Th51;
hence y in cl_Ball(x,r) by Th47;
end;
hence thesis by SUBSET_1:7;
end;
theorem
Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r)
proof
A1: Ball(x,r) \/ Sphere(x,r) c= cl_Ball(x,r)
proof
Ball(x,r) c= cl_Ball(x,r) &
Sphere(x,r) c= cl_Ball(x,r) by Th54,Th55;
hence thesis by XBOOLE_1:8;
end;
now let y; assume y in cl_Ball(x,r);
then A2: ||.x - y.|| <= r by Th47;
now per cases by A2,REAL_1:def 5;
case ||.x - y.|| < r;
hence y in Ball(x,r) by Th40;
case ||.x - y.|| = r;
hence y in Sphere(x,r) by Th51;
end;
hence y in Ball(x,r) \/ Sphere(x,r) by XBOOLE_0:def 2;
end;
then cl_Ball(x,r) c= Ball(x,r) \/ Sphere(x,r) by SUBSET_1:7;
hence thesis by A1,XBOOLE_0:def 10;
end;