### The Mizar article:

### Introduction to Banach and Hilbert Spaces --- Part II

**by****Jan Popiolek**

- Received July 19, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: BHSP_2
- [ MML identifier index ]

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;

Back to top