:: Sequences in $R^n$
:: by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski
::
:: Received May 10, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

definition
let N be Nat;
mode Real_Sequence of N is sequence of (TOP-REAL N);
end;

theorem Th1: :: TOPRNS_1:1
for N being Element of NAT
for f being Function holds
( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) )
proofend;

definition
let N be Element of NAT ;
let IT be Real_Sequence of N;
attrIT is non-zero  means :Def1: :: TOPRNS_1:def 1
 rng IT c= NonZero (TOP-REAL N);
end;

:: deftheorem Def1 defines non-zero TOPRNS_1:def_1_:_
 for N being Element of NAT
for IT being Real_Sequence of N holds
( IT is non-zero iff rng IT c= NonZero (TOP-REAL N) );

theorem Th2: :: TOPRNS_1:2
for N being Element of NAT
for seq being Real_Sequence of N holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) )
proofend;

theorem Th3: :: TOPRNS_1:3
for N being Element of NAT
for seq being Real_Sequence of N holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) )
proofend;

definition
let N be Nat;
let seq1, seq2 be Real_Sequence of N;
funcseq1 + seq2 ->  Real_Sequence of N equals :: TOPRNS_1:def 2
seq1 + seq2;
coherence
 seq1 + seq2 is Real_Sequence of N
proofend;
end;

:: deftheorem  defines + TOPRNS_1:def_2_:_
 for N being Nat
for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq1 + seq2;

definition
let r be Real;
let N be Nat;
let seq be Real_Sequence of N;
funcr * seq ->  Real_Sequence of N equals :: TOPRNS_1:def 3
r (#) seq;
coherence
 r (#) seq is Real_Sequence of N
proofend;
end;

:: deftheorem  defines * TOPRNS_1:def_3_:_
 for r being Real
for N being Nat
for seq being Real_Sequence of N holds r * seq = r (#) seq;

definition
let N be Nat;
let seq be Real_Sequence of N;
func - seq ->  Real_Sequence of N equals :: TOPRNS_1:def 4
 - seq;
coherence
 - seq is Real_Sequence of N
proofend;
end;

:: deftheorem  defines - TOPRNS_1:def_4_:_
 for N being Nat
for seq being Real_Sequence of N holds - seq = - seq;

definition
let N be Nat;
let seq1, seq2 be Real_Sequence of N;
funcseq1 - seq2 ->  Real_Sequence of N equals :: TOPRNS_1:def 5
seq1 + (- seq2);
correctness
coherence
seq1 + (- seq2) is Real_Sequence of N;
;
end;

:: deftheorem  defines - TOPRNS_1:def_5_:_
 for N being Nat
for seq1, seq2 being Real_Sequence of N holds seq1 - seq2 = seq1 + (- seq2);

definition
let N be Nat;
let seq be Real_Sequence of N;
func|.seq.| ->  Real_Sequence means :Def6: :: TOPRNS_1:def 6
 for n being Element of NAT holds it . n = |.(seq . n).|;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = |.(seq . n).|
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = |.(seq . n).| ) &amp; ( for n being Element of NAT holds b2 . n = |.(seq . n).| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines |. TOPRNS_1:def_6_:_
 for N being Nat
for seq being Real_Sequence of N
for b3 being Real_Sequence holds
( b3 = |.seq.| iff for n being Element of NAT holds b3 . n = |.(seq . n).| );

theorem Th4: :: TOPRNS_1:4
for N, n being Nat
for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)
proofend;

theorem Th5: :: TOPRNS_1:5
for r being Real
for N, n being Nat
for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)
proofend;

theorem Th6: :: TOPRNS_1:6
for N, n being Nat
for seq being Real_Sequence of N holds (- seq) . n = - (seq . n)
proofend;

theorem Th7: :: TOPRNS_1:7
for N being Element of NAT
for r being Real
for w being Point of (TOP-REAL N) holds (abs r) * |.w.| = |.(r * w).| by EUCLID:11;

theorem :: TOPRNS_1:8
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.|
proofend;

theorem :: TOPRNS_1:9
for N being Element of NAT
for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1
proofend;

theorem Th10: :: TOPRNS_1:10
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proofend;

theorem Th11: :: TOPRNS_1:11
for N being Element of NAT
for seq being Real_Sequence of N holds - seq = (- 1) * seq
proofend;

theorem Th12: :: TOPRNS_1:12
for N being Element of NAT
for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)
proofend;

theorem Th13: :: TOPRNS_1:13
for N being Element of NAT
for r, q being Real
for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)
proofend;

theorem Th14: :: TOPRNS_1:14
for N being Element of NAT
for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2)
proofend;

theorem :: TOPRNS_1:15
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proofend;

theorem Th16: :: TOPRNS_1:16
for N being Element of NAT
for seq being Real_Sequence of N holds 1 * seq = seq
proofend;

theorem Th17: :: TOPRNS_1:17
for N being Element of NAT
for seq being Real_Sequence of N holds - (- seq) = seq
proofend;

theorem :: TOPRNS_1:18
for N being Element of NAT
for seq1, seq2 being Real_Sequence of N holds seq1 - (- seq2) = seq1 + seq2 by Th17;

theorem :: TOPRNS_1:19
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proofend;

theorem :: TOPRNS_1:20
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 by Th10;

theorem Th21: :: TOPRNS_1:21
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N st r <> 0 &amp; seq is non-zero holds
r * seq is non-zero
proofend;

theorem :: TOPRNS_1:22
for N being Element of NAT
for seq being Real_Sequence of N st seq is non-zero holds
- seq is non-zero
proofend;

theorem Th23: :: TOPRNS_1:23
for N being Element of NAT holds |.(0. (TOP-REAL N)).| = 0
proofend;

theorem Th24: :: TOPRNS_1:24
for N being Element of NAT
for w being Point of (TOP-REAL N) st |.w.| = 0 holds
w = 0. (TOP-REAL N)
proofend;

theorem :: TOPRNS_1:25
for N being Element of NAT
for w being Point of (TOP-REAL N) holds |.w.| >= 0 ;

theorem :: TOPRNS_1:26
for N being Element of NAT
for w being Point of (TOP-REAL N) holds |.(- w).| = |.w.| by EUCLID:71;

theorem Th27: :: TOPRNS_1:27
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| = |.(w2 - w1).|
proofend;

Lm1:  for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds
w1 = w2
proofend;

Lm2:  for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0
proofend;

theorem :: TOPRNS_1:28
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds
( |.(w1 - w2).| = 0 iff w1 = w2 ) by Lm1, Lm2;

theorem Th29: :: TOPRNS_1:29
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 + w2).| <= |.w1.| + |.w2.|
proofend;

theorem :: TOPRNS_1:30
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.w1.| + |.w2.|
proofend;

theorem :: TOPRNS_1:31
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 + w2).|
proofend;

theorem Th32: :: TOPRNS_1:32
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 - w2).|
proofend;

theorem :: TOPRNS_1:33
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st w1 <> w2 holds
|.(w1 - w2).| > 0
proofend;

theorem :: TOPRNS_1:34
for N being Element of NAT
for w1, w2, w being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
proofend;

definition
let N be Element of NAT ;
let IT be Real_Sequence of N;
attrIT is bounded  means :Def7: :: TOPRNS_1:def 7
 ex r being Real st
for n being Element of NAT holds |.(IT . n).| < r;
end;

:: deftheorem Def7 defines bounded TOPRNS_1:def_7_:_
 for N being Element of NAT
for IT being Real_Sequence of N holds
( IT is bounded iff ex r being Real st
for n being Element of NAT holds |.(IT . n).| < r );

theorem Th35: :: TOPRNS_1:35
for N being Element of NAT
for seq being Real_Sequence of N
for n being Element of NAT ex r being Real st
( 0 < r &amp; ( for m being Element of NAT st m <= n holds
|.(seq . m).| < r ) )
proofend;

definition
let N be Element of NAT ;
let IT be Real_Sequence of N;
attrIT is convergent  means :Def8: :: TOPRNS_1:def 8
 ex g being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((IT . m) - g).| < r;
end;

:: deftheorem Def8 defines convergent TOPRNS_1:def_8_:_
 for N being Element of NAT
for IT being Real_Sequence of N holds
( IT is convergent iff ex g being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((IT . m) - g).| < r );

definition
let N be Element of NAT ;
let seq be Real_Sequence of N;
assume A1: seq is convergent ;
func lim seq ->  Point of (TOP-REAL N) means :Def9: :: TOPRNS_1:def 9
 for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - it).| < r;
existence
 ex b1 being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b1).| < r by A1, Def8;
uniqueness
 for b1, b2 being Point of (TOP-REAL N) st ( for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b1).| < r ) &amp; ( for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b2).| < r ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines lim TOPRNS_1:def_9_:_
 for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
for b3 being Point of (TOP-REAL N) holds
( b3 = lim seq iff for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b3).| < r );

theorem Th36: :: TOPRNS_1:36
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent &amp; seq9 is convergent holds
seq + seq9 is convergent
proofend;

theorem Th37: :: TOPRNS_1:37
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent &amp; seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)
proofend;

theorem Th38: :: TOPRNS_1:38
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent
proofend;

theorem Th39: :: TOPRNS_1:39
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)
proofend;

theorem Th40: :: TOPRNS_1:40
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
- seq is convergent
proofend;

theorem Th41: :: TOPRNS_1:41
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
lim (- seq) = - (lim seq)
proofend;

theorem :: TOPRNS_1:42
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent &amp; seq9 is convergent holds
seq - seq9 is convergent
proofend;

theorem :: TOPRNS_1:43
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent &amp; seq9 is convergent holds
lim (seq - seq9) = (lim seq) - (lim seq9)
proofend;

theorem :: TOPRNS_1:44
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
seq is bounded
proofend;

theorem :: TOPRNS_1:45
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent &amp; lim seq <> 0. (TOP-REAL N) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
proofend;