:: by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski

::

:: Received May 10, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

theorem Th1: :: TOPRNS_1:1

for N being Nat

for f being Function holds

( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) ) )

for f being Function holds

( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) ) )

proof end;

:: deftheorem defines non-zero TOPRNS_1:def 1 :

for N being Nat

for IT being Real_Sequence of N holds

( IT is non-zero iff rng IT c= NonZero (TOP-REAL N) );

for N being 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 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) )

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) )

proof end;

theorem Th3: :: TOPRNS_1:3

for N being Nat

for seq being Real_Sequence of N holds

( seq is non-zero iff for n being Nat holds seq . n <> 0. (TOP-REAL N) )

for seq being Real_Sequence of N holds

( seq is non-zero iff for n being Nat holds seq . n <> 0. (TOP-REAL N) )

proof end;

definition

let N be Nat;

let seq1, seq2 be Real_Sequence of N;

coherence

seq1 + seq2 is Real_Sequence of N

end;
let seq1, seq2 be Real_Sequence of N;

coherence

seq1 + seq2 is Real_Sequence of N

proof end;

:: deftheorem defines + TOPRNS_1:def 2 :

for N being Nat

for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq1 + seq2;

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;

coherence

r (#) seq is Real_Sequence of N

end;
let N be Nat;

let seq be Real_Sequence of N;

coherence

r (#) seq is Real_Sequence of N

proof 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;

for r being Real

for N being Nat

for seq being Real_Sequence of N holds r * seq = r (#) seq;

definition
end;

:: deftheorem defines - TOPRNS_1:def 4 :

for N being Nat

for seq being Real_Sequence of N holds - seq = - seq;

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;

correctness

coherence

seq1 + (- seq2) is Real_Sequence of N;

;

end;
let seq1, seq2 be Real_Sequence of N;

correctness

coherence

seq1 + (- seq2) is Real_Sequence of N;

;

:: deftheorem defines - TOPRNS_1:def 5 :

for N being Nat

for seq1, seq2 being Real_Sequence of N holds seq1 - seq2 = seq1 + (- seq2);

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;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = |.(seq . n).|

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = |.(seq . n).| ) & ( for n being Nat holds b_{2} . n = |.(seq . n).| ) holds

b_{1} = b_{2}

end;
let seq be Real_Sequence of N;

func |.seq.| -> Real_Sequence means :Def6: :: TOPRNS_1:def 6

for n being Nat holds it . n = |.(seq . n).|;

existence for n being Nat holds it . n = |.(seq . n).|;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines |. TOPRNS_1:def 6 :

for N being Nat

for seq being Real_Sequence of N

for b_{3} being Real_Sequence holds

( b_{3} = |.seq.| iff for n being Nat holds b_{3} . n = |.(seq . n).| );

for N being Nat

for seq being Real_Sequence of N

for b

( b

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)

for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)

proof end;

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)

for N, n being Nat

for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)

proof end;

theorem :: TOPRNS_1:8

for N being Nat

for r being Real

for seq being Real_Sequence of N holds |.(r * seq).| = |.r.| (#) |.seq.|

for r being Real

for seq being Real_Sequence of N holds |.(r * seq).| = |.r.| (#) |.seq.|

proof end;

theorem :: TOPRNS_1:9

theorem Th10: :: TOPRNS_1:10

for N being Nat

for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)

for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)

proof end;

theorem Th12: :: TOPRNS_1:12

for N being Nat

for r being Real

for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)

for r being Real

for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)

proof end;

theorem Th13: :: TOPRNS_1:13

for N being Nat

for q, r being Real

for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)

for q, r being Real

for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)

proof end;

theorem Th14: :: TOPRNS_1:14

for N being Nat

for r being Real

for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2)

for r being Real

for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2)

proof end;

theorem :: TOPRNS_1:15

for N being Nat

for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

proof end;

theorem :: TOPRNS_1:18

theorem :: TOPRNS_1:19

for N being Nat

for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

proof end;

theorem :: TOPRNS_1:20

theorem Th21: :: TOPRNS_1:21

for N being Nat

for r being Real

for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds

r * seq is non-zero

for r being Real

for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds

r * seq is non-zero

proof end;

theorem :: TOPRNS_1:26

Lm1: for N being Nat

for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds

w1 = w2

proof end;

Lm2: for N being Nat

for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds

|.(w1 - w2).| = 0

proof end;

theorem :: TOPRNS_1:28

theorem :: TOPRNS_1:34

for N being Nat

for w, w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|

for w, w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|

proof end;

:: deftheorem defines bounded TOPRNS_1:def 7 :

for N being Nat

for IT being Real_Sequence of N holds

( IT is bounded iff ex r being Real st

for n being Nat holds |.(IT . n).| < r );

for N being Nat

for IT being Real_Sequence of N holds

( IT is bounded iff ex r being Real st

for n being Nat holds |.(IT . n).| < r );

theorem Th35: :: TOPRNS_1:35

for N being Nat

for seq being Real_Sequence of N

for n being Nat ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(seq . m).| < r ) )

for seq being Real_Sequence of N

for n being Nat ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(seq . m).| < r ) )

proof end;

:: deftheorem defines convergent TOPRNS_1:def 8 :

for N being 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 Nat st

for m being Nat st n <= m holds

|.((IT . m) - g).| < r );

for N being 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 Nat st

for m being Nat st n <= m holds

|.((IT . m) - g).| < r );

definition

let N be Nat;

let seq be Real_Sequence of N;

assume A1: seq is convergent ;

ex b_{1} being Point of (TOP-REAL N) st

for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < r
by A1;

uniqueness

for b_{1}, b_{2} being Point of (TOP-REAL N) st ( for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < r ) & ( for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{2}).| < r ) holds

b_{1} = b_{2}

end;
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 Nat st

for m being Nat st n <= m holds

|.((seq . m) - it).| < r;

existence for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - it).| < r;

ex b

for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

uniqueness

for b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

b

proof end;

:: deftheorem Def9 defines lim TOPRNS_1:def 9 :

for N being Nat

for seq being Real_Sequence of N st seq is convergent holds

for b_{3} being Point of (TOP-REAL N) holds

( b_{3} = lim seq iff for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{3}).| < r );

for N being Nat

for seq being Real_Sequence of N st seq is convergent holds

for b

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

theorem Th36: :: TOPRNS_1:36

for N being Nat

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

seq + seq9 is convergent

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

seq + seq9 is convergent

proof end;

theorem Th37: :: TOPRNS_1:37

for N being Nat

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

lim (seq + seq9) = (lim seq) + (lim seq9)

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

lim (seq + seq9) = (lim seq) + (lim seq9)

proof end;

theorem Th38: :: TOPRNS_1:38

for N being Nat

for r being Real

for seq being Real_Sequence of N st seq is convergent holds

r * seq is convergent

for r being Real

for seq being Real_Sequence of N st seq is convergent holds

r * seq is convergent

proof end;

theorem Th39: :: TOPRNS_1:39

for N being Nat

for r being Real

for seq being Real_Sequence of N st seq is convergent holds

lim (r * seq) = r * (lim seq)

for r being Real

for seq being Real_Sequence of N st seq is convergent holds

lim (r * seq) = r * (lim seq)

proof end;

theorem Th41: :: TOPRNS_1:41

for N being Nat

for seq being Real_Sequence of N st seq is convergent holds

lim (- seq) = - (lim seq)

for seq being Real_Sequence of N st seq is convergent holds

lim (- seq) = - (lim seq)

proof end;

theorem :: TOPRNS_1:42

for N being Nat

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

seq - seq9 is convergent

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

seq - seq9 is convergent

proof end;

theorem :: TOPRNS_1:43

for N being Nat

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

lim (seq - seq9) = (lim seq) - (lim seq9)

for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds

lim (seq - seq9) = (lim seq) - (lim seq9)

proof end;

theorem :: TOPRNS_1:45

for N being Nat

for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds

ex n being Nat st

for m being Nat st n <= m holds

|.(lim seq).| / 2 < |.(seq . m).|

for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds

ex n being Nat st

for m being Nat st n <= m holds

|.(lim seq).| / 2 < |.(seq . m).|

proof end;