REAL_NS1: Completeness of the Real {E}uclidean Space

:: Completeness of the Real {E}uclidean Space
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 28, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

Lm1: for n being Nat ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative )

proof end;

definition

let n be Nat;

func Euclid_add n -> BinOp of (REAL n) means :Def1: :: REAL_NS1:def 1
for a, b being Element of REAL n holds it . (a,b) = a + b;

proof end;

proof end;

end;

:: deftheorem Def1 defines Euclid_add REAL_NS1:def 1 :

registration

let n be Nat;

cluster Euclid_add n -> commutative associative ;

proof end;

end;

definition

let n be Nat;

func Euclid_mult n -> Function of [:REAL,(REAL n):],(REAL n) means :Def2: :: REAL_NS1:def 2
for r being Real
for x being Element of REAL n holds it . (r,x) = r * x;

proof end;

proof end;

end;

:: deftheorem Def2 defines Euclid_mult REAL_NS1:def 2 :

definition

let n be Nat;

func Euclid_norm n -> Function of (REAL n),REAL means :Def3: :: REAL_NS1:def 3
for x being Element of REAL n holds it . x = |.x.|;

proof end;

proof end;

end;

:: deftheorem Def3 defines Euclid_norm REAL_NS1:def 3 :

definition

let n be Nat;

func REAL-NS n -> non empty strict NORMSTR means :Def4: :: REAL_NS1:def 4
( the carrier of it = REAL n & 0. it = 0* n & the addF of it = Euclid_add n & the Mult of it = Euclid_mult n & the normF of it = Euclid_norm n );

proof end;

end;

:: deftheorem Def4 defines REAL-NS REAL_NS1:def 4 :

registration

let n be non zero Nat;

cluster REAL-NS n -> non empty non trivial strict ;

proof end;

end;

theorem Th1: :: REAL_NS1:1

for n being Nat
for x being VECTOR of (REAL-NS n)
for y being Element of REAL n st x = y holds
||.x.|| = |.y.|

proof end;

theorem Th2: :: REAL_NS1:2

for n being Nat
for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b

proof end;

theorem Th3: :: REAL_NS1:3

for n being Nat
for x being VECTOR of (REAL-NS n)
for y being Element of REAL n
for a being Real st x = y holds
a * x = a * y

proof end;

registration

let n be Nat;

cluster REAL-NS n -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;

proof end;

end;

theorem Th4: :: REAL_NS1:4

for n being Nat
for x being VECTOR of (REAL-NS n)
for a being Element of REAL n st x = a holds
- x = - a

proof end;

theorem Th5: :: REAL_NS1:5

for n being Nat
for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x - y = a - b

proof end;

theorem Th6: :: REAL_NS1:6

for n being Nat
for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n

proof end;

theorem Th7: :: REAL_NS1:7

for n being Nat
for x being Element of REAL n st ( for i being Nat st i in Seg n holds
0 <= x . i ) holds
( 0 <= Sum x & ( for i being Nat st i in Seg n holds
x . i <= Sum x ) )

proof end;

theorem Th8: :: REAL_NS1:8

for n being Nat
for x being Element of REAL n
for i being Nat st i in Seg n holds
|.(x . i).| <= |.x.|

proof end;

theorem Th9: :: REAL_NS1:9

for n being Nat
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.||

proof end;

theorem Th10: :: REAL_NS1:10

for n being Nat
for x being Element of REAL (n + 1) holds |.x.| ^2 = (|.(x | n).| ^2) + ((x . (n + 1)) ^2)

proof end;

definition

let n be Nat;
let f be sequence of (REAL n);
let k be Nat;
:: original: .
redefine func f . k -> Element of REAL n;
coherence

proof end;

end;

theorem Th11: :: REAL_NS1:11

for n being Nat
for x being Point of (REAL-NS n)
for xs being Element of REAL n
for seq being sequence of (REAL-NS n)
for xseq being sequence of (REAL n) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )

proof end;

theorem Th12: :: REAL_NS1:12

for n being Nat
for f being sequence of (REAL-NS n) st f is Cauchy_sequence_by_Norm holds
f is convergent

proof end;

Lm2: for n being Nat holds REAL-NS n is RealBanachSpace

proof end;

registration

let n be Nat;

cluster REAL-NS n -> non empty strict complete ;

coherence by Lm2;

end;

definition

let n be Nat;

func Euclid_scalar n -> Function of [:(REAL n),(REAL n):],REAL means :Def5: :: REAL_NS1:def 5
for x, y being Element of REAL n holds it . (x,y) = Sum (mlt (x,y));

proof end;

proof end;

end;

:: deftheorem Def5 defines Euclid_scalar REAL_NS1:def 5 :

definition

let n be Nat;

func REAL-US n -> non empty strict UNITSTR means :Def6: :: REAL_NS1:def 6
( the carrier of it = REAL n & 0. it = 0* n & the addF of it = Euclid_add n & the Mult of it = Euclid_mult n & the scalar of it = Euclid_scalar n );

proof end;

end;

:: deftheorem Def6 defines REAL-US REAL_NS1:def 6 :

registration

let n be non zero Nat;

cluster REAL-US n -> non empty non trivial strict ;

proof end;

end;

registration

let n be Nat;

cluster REAL-US n -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ;

proof end;

end;

theorem Th13: :: REAL_NS1:13

for n being Nat
for a being Real
for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )

proof end;

theorem :: REAL_NS1:14

for n being Nat
for x1 being Point of (REAL-NS n)
for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2

proof end;

theorem Th15: :: REAL_NS1:15

for n being Nat
for f being set holds
( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )

proof end;

theorem Th16: :: REAL_NS1:16

for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds
( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

proof end;

theorem :: REAL_NS1:17

for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy

proof end;

theorem Th18: :: REAL_NS1:18

for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds
seq1 is Cauchy_sequence_by_Norm

proof end;

registration

let n be Nat;

cluster REAL-US n -> non empty strict complete ;

proof end;

end;