:: 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
)
) ) )
proof
end;
definition
let
N
be
Element
of
NAT
;
let
IT
be
Real_Sequence
of
N
;
attr
IT
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
)
)
proof
end;
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
)
)
proof
end;
definition
let
N
be
Nat
;
let
seq1
,
seq2
be
Real_Sequence
of
N
;
func
seq1
+
seq2
->
Real_Sequence
of
N
equals
:: TOPRNS_1:def 2
seq1
+
seq2
;
coherence
seq1
+
seq2
is
Real_Sequence
of
N
proof
end;
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
;
func
r
*
seq
->
Real_Sequence
of
N
equals
:: TOPRNS_1:def 3
r
(#)
seq
;
coherence
r
(#)
seq
is
Real_Sequence
of
N
proof
end;
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
proof
end;
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
;
func
seq1
-
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
b
1
being
Real_Sequence
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
|.
(
seq
.
n
)
.|
proof
end;
uniqueness
for
b
1
,
b
2
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
|.
(
seq
.
n
)
.|
) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
|.
(
seq
.
n
)
.|
) holds
b
1
=
b
2
proof
end;
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
Element
of
NAT
holds
b
3
.
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
)
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
)
proof
end;
theorem
Th6
:
:: TOPRNS_1:6
for
N
,
n
being
Nat
for
seq
being
Real_Sequence
of
N
holds
(
-
seq
)
.
n
=
-
(
seq
.
n
)
proof
end;
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
.|
proof
end;
theorem
:: TOPRNS_1:9
for
N
being
Element
of
NAT
for
seq1
,
seq2
being
Real_Sequence
of
N
holds
seq1
+
seq2
=
seq2
+
seq1
proof
end;
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
)
proof
end;
theorem
Th11
:
:: TOPRNS_1:11
for
N
being
Element
of
NAT
for
seq
being
Real_Sequence
of
N
holds
-
seq
=
(
-
1
)
*
seq
proof
end;
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
)
proof
end;
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
)
proof
end;
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
)
proof
end;
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
proof
end;
theorem
Th16
:
:: TOPRNS_1:16
for
N
being
Element
of
NAT
for
seq
being
Real_Sequence
of
N
holds 1
*
seq
=
seq
proof
end;
theorem
Th17
:
:: TOPRNS_1:17
for
N
being
Element
of
NAT
for
seq
being
Real_Sequence
of
N
holds
-
(
-
seq
)
=
seq
proof
end;
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
proof
end;
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
&
seq
is
non-zero
holds
r
*
seq
is
non-zero
proof
end;
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
proof
end;
theorem
Th23
:
:: TOPRNS_1:23
for
N
being
Element
of
NAT
holds
|.
(
0.
(
TOP-REAL
N
)
)
.|
=
0
proof
end;
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
)
proof
end;
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
)
.|
proof
end;
Lm1
:
for
N
being
Element
of
NAT
for
w1
,
w2
being
Point
of
(
TOP-REAL
N
)
st
|.
(
w1
-
w2
)
.|
=
0
holds
w1
=
w2
proof
end;
Lm2
:
for
N
being
Element
of
NAT
for
w1
,
w2
being
Point
of
(
TOP-REAL
N
)
st
w1
=
w2
holds
|.
(
w1
-
w2
)
.|
=
0
proof
end;
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
.|
proof
end;
theorem
:: TOPRNS_1:30
for
N
being
Element
of
NAT
for
w1
,
w2
being
Point
of
(
TOP-REAL
N
)
holds
|.
(
w1
-
w2
)
.|
<=
|.
w1
.|
+
|.
w2
.|
proof
end;
theorem
:: TOPRNS_1:31
for
N
being
Element
of
NAT
for
w1
,
w2
being
Point
of
(
TOP-REAL
N
)
holds
|.
w1
.|
-
|.
w2
.|
<=
|.
(
w1
+
w2
)
.|
proof
end;
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
)
.|
proof
end;
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
proof
end;
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
)
.|
proof
end;
definition
let
N
be
Element
of
NAT
;
let
IT
be
Real_Sequence
of
N
;
attr
IT
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
& ( for
m
being
Element
of
NAT
st
m
<=
n
holds
|.
(
seq
.
m
)
.|
<
r
) )
proof
end;
definition
let
N
be
Element
of
NAT
;
let
IT
be
Real_Sequence
of
N
;
attr
IT
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
b
1
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
)
-
b
1
)
.|
<
r
by
A1
,
Def8
;
uniqueness
for
b
1
,
b
2
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
)
-
b
1
)
.|
<
r
) & ( 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
)
-
b
2
)
.|
<
r
) holds
b
1
=
b
2
proof
end;
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
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
Element
of
NAT
st
for
m
being
Element
of
NAT
st
n
<=
m
holds
|.
(
(
seq
.
m
)
-
b
3
)
.|
<
r
);
theorem
Th36
:
:: TOPRNS_1:36
for
N
being
Element
of
NAT
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
Element
of
NAT
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
Element
of
NAT
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
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
)
proof
end;
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
proof
end;
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
)
proof
end;
theorem
:: TOPRNS_1:42
for
N
being
Element
of
NAT
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
Element
of
NAT
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:44
for
N
being
Element
of
NAT
for
seq
being
Real_Sequence
of
N
st
seq
is
convergent
holds
seq
is
bounded
proof
end;
theorem
:: TOPRNS_1:45
for
N
being
Element
of
NAT
for
seq
being
Real_Sequence
of
N
st
seq
is
convergent
&
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
)
.|
proof
end;