:: TOPRNS_1 semantic presentation

definition

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

end;

theorem :: TOPRNS_1:1

canceled;

theorem Th2: :: TOPRNS_1:2

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

proof end;

definition

let N be Nat;
let IT be Real_Sequence of N;
attr IT is non-zero means :Def1: :: TOPRNS_1:def 1
rng IT c= the carrier of (TOP-REAL N) \ {(0.REAL N)};

end;

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

theorem Th3: :: TOPRNS_1:3

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.REAL N )

proof end;

theorem Th4: :: TOPRNS_1:4

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.REAL N )

proof end;

theorem Th5: :: TOPRNS_1:5

for N being Nat
for seq, seq1 being Real_Sequence of N st ( for x being set st x in NAT holds
seq . x = seq1 . x ) holds
seq = seq1

proof end;

theorem Th6: :: TOPRNS_1:6

for N being Nat
for seq, seq1 being Real_Sequence of N st ( for n being Nat holds seq . n = seq1 . n ) holds
seq = seq1

proof end;

scheme :: TOPRNS_1:sch 1
ExTopRealNSeq{ F₁() -> Nat, F₂( Nat) -> Point of (TOP-REAL F₁()) } :

ex seq being Real_Sequence of F₁() st
for n being Nat holds seq . n = F₂(n)

proof end;

definition

let N be Nat;
let seq1, seq2 be Real_Sequence of N;
func seq1 + seq2 -> Real_Sequence of N means :Def2: :: TOPRNS_1:def 2
for n being Nat holds it . n = (seq1 . n) + (seq2 . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines + TOPRNS_1:def 2 :

definition

let r be Real;
let N be Nat;
let seq be Real_Sequence of N;
func r * seq -> Real_Sequence of N means :Def3: :: TOPRNS_1:def 3
for n being Nat holds it . n = r * (seq . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines * TOPRNS_1:def 3 :

definition

let N be Nat;
let seq be Real_Sequence of N;
func - seq -> Real_Sequence of N means :Def4: :: TOPRNS_1:def 4
for n being Nat holds it . n = - (seq . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines - TOPRNS_1:def 4 :

definition

let N be Nat;
let seq1, seq2 be Real_Sequence of N;
func seq1 - seq2 -> Real_Sequence of N equals :: TOPRNS_1:def 5
seq1 + (- seq2);
correctness ;

end;

:: deftheorem defines - TOPRNS_1:def 5 :

definition

let N be Nat;
let x be Point of (TOP-REAL N);
func |.x.| -> Real means :Def6: :: TOPRNS_1:def 6
ex y being FinSequence of REAL st
( x = y & it = |.y.| );
existence

proof end;

uniqueness ;

end;

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

definition

let N be Nat;
let seq be Real_Sequence of N;
func |.seq.| -> Real_Sequence means :Def7: :: TOPRNS_1:def 7
for n being Nat holds it . n = |.(seq . n).|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines |. TOPRNS_1:def 7 :

theorem :: TOPRNS_1:7

canceled;

theorem Th8: :: TOPRNS_1:8

for N being Nat
for r being Real
for w being Point of (TOP-REAL N) holds (abs r) * |.w.| = |.(r * w).|

proof end;

theorem :: TOPRNS_1:9

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

proof end;

theorem :: TOPRNS_1:10

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

proof end;

theorem Th11: :: TOPRNS_1:11

for N being Nat
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 seq being Real_Sequence of N holds - seq = (- 1) * seq

proof end;

theorem Th13: :: TOPRNS_1:13

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

proof end;

theorem Th14: :: TOPRNS_1:14

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

proof end;

theorem Th15: :: TOPRNS_1:15

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

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

proof end;

theorem Th17: :: TOPRNS_1:17

for N being Nat
for seq being Real_Sequence of N holds 1 * seq = seq

proof end;

theorem Th18: :: TOPRNS_1:18

for N being Nat
for seq being Real_Sequence of N holds - (- seq) = seq

proof end;

theorem Th19: :: TOPRNS_1:19

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

theorem :: TOPRNS_1:20

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

proof end;

theorem :: TOPRNS_1:21

for N being Nat
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 by Th11;

theorem Th22: :: TOPRNS_1:22

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

proof end;

theorem :: TOPRNS_1:23

for N being Nat
for seq being Real_Sequence of N st seq is non-zero holds
- seq is non-zero

proof end;

theorem Th24: :: TOPRNS_1:24

for N being Nat holds |.(0.REAL N).| = 0

proof end;

theorem Th25: :: TOPRNS_1:25

for N being Nat
for w being Point of (TOP-REAL N) st |.w.| = 0 holds
w = 0.REAL N

proof end;

theorem Th26: :: TOPRNS_1:26

for N being Nat
for w being Point of (TOP-REAL N) holds |.w.| >= 0

proof end;

theorem Th27: :: TOPRNS_1:27

for N being Nat
for w being Point of (TOP-REAL N) holds |.(- w).| = |.w.|

proof end;

theorem Th28: :: TOPRNS_1:28

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

proof end;

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:29

for N being Nat
for w1, w2 being Point of (TOP-REAL N) holds
( |.(w1 - w2).| = 0 iff w1 = w2 ) by Lm1, Lm2;

theorem Th30: :: TOPRNS_1:30

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

proof end;

theorem :: TOPRNS_1:31

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

proof end;

theorem :: TOPRNS_1:32

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

proof end;

theorem Th33: :: TOPRNS_1:33

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

proof end;

theorem :: TOPRNS_1:34

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:35

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

proof end;

theorem :: TOPRNS_1:36

for N being Nat
for r1, r2 being Real
for w1, w2 being Point of (TOP-REAL N) st 0 <= r1 & |.w1.| < |.w2.| & r1 < r2 holds
|.w1.| * r1 < |.w2.| * r2

proof end;

theorem :: TOPRNS_1:37

canceled;

theorem :: TOPRNS_1:38

for N being Nat
for r being Real
for w being Point of (TOP-REAL N) holds
( ( - |.w.| < r & r < |.w.| ) iff abs r < |.w.| )

proof end;

definition

let N be Nat;
let IT be Real_Sequence of N;
attr IT is bounded means :Def8: :: TOPRNS_1:def 8
ex r being Real st
for n being Nat holds |.(IT . n).| < r;

end;

:: deftheorem Def8 defines bounded TOPRNS_1:def 8 :

theorem Th39: :: TOPRNS_1:39

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

proof end;

definition

let N be Nat;
let IT be Real_Sequence of N;
attr IT is convergent means :Def9: :: TOPRNS_1:def 9
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;

end;

:: deftheorem Def9 defines convergent TOPRNS_1:def 9 :

definition

let N be Nat;
let seq be Real_Sequence of N;
assume A1: seq is convergent ;
func lim seq -> Point of (TOP-REAL N) means :Def10: :: TOPRNS_1:def 10
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 by A1, Def9;
uniqueness

proof end;

end;

:: deftheorem Def10 defines lim TOPRNS_1:def 10 :

theorem :: TOPRNS_1:40

canceled;

theorem Th41: :: TOPRNS_1:41

for N being Nat
for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
seq + seq' is convergent

proof end;

theorem Th42: :: TOPRNS_1:42

for N being Nat
for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
lim (seq + seq') = (lim seq) + (lim seq')

proof end;

theorem Th43: :: TOPRNS_1:43

for N being Nat
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent

proof end;

theorem Th44: :: TOPRNS_1:44

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)

proof end;

theorem Th45: :: TOPRNS_1:45

for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
- seq is convergent

proof end;

theorem Th46: :: TOPRNS_1:46

for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
lim (- seq) = - (lim seq)

proof end;

theorem :: TOPRNS_1:47

for N being Nat
for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
seq - seq' is convergent

proof end;

theorem :: TOPRNS_1:48

for N being Nat
for seq, seq' being Real_Sequence of N st seq is convergent & seq' is convergent holds
lim (seq - seq') = (lim seq) - (lim seq')

proof end;

theorem :: TOPRNS_1:49

canceled;

theorem :: TOPRNS_1:50

for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
seq is bounded

proof end;

theorem :: TOPRNS_1:51

for N being Nat
for seq being Real_Sequence of N st seq is convergent & lim seq <> 0.REAL N holds
ex n being Nat st
for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|

proof end;