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


begin

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;
existence
ex b1 being BinOp of (REAL n) st
for a, b being Element of REAL n holds b1 . (a,b) = a + b
proof end;
uniqueness
for b1, b2 being BinOp of (REAL n) st ( for a, b being Element of REAL n holds b1 . (a,b) = a + b ) & ( for a, b being Element of REAL n holds b2 . (a,b) = a + b ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Euclid_add REAL_NS1:def 1 :
for n being Nat
for b2 being BinOp of (REAL n) holds
( b2 = Euclid_add n iff for a, b being Element of REAL n holds b2 . (a,b) = a + b );

registration
let n be Nat;
cluster Euclid_add n -> commutative associative ;
coherence
( Euclid_add n is commutative & Euclid_add n is 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 Element of REAL
for x being Element of REAL n holds it . (r,x) = r * x;
existence
ex b1 being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds b1 . (r,x) = r * x
proof end;
uniqueness
for b1, b2 being Function of [:REAL,(REAL n):],(REAL n) st ( for r being Element of REAL
for x being Element of REAL n holds b1 . (r,x) = r * x ) & ( for r being Element of REAL
for x being Element of REAL n holds b2 . (r,x) = r * x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Euclid_mult REAL_NS1:def 2 :
for n being Nat
for b2 being Function of [:REAL,(REAL n):],(REAL n) holds
( b2 = Euclid_mult n iff for r being Element of REAL
for x being Element of REAL n holds b2 . (r,x) = r * x );

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.|;
existence
ex b1 being Function of (REAL n),REAL st
for x being Element of REAL n holds b1 . x = |.x.|
proof end;
uniqueness
for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds b1 . x = |.x.| ) & ( for x being Element of REAL n holds b2 . x = |.x.| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Euclid_norm REAL_NS1:def 3 :
for n being Nat
for b2 being Function of (REAL n),REAL holds
( b2 = Euclid_norm n iff for x being Element of REAL n holds b2 . x = |.x.| );

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 );
existence
ex b1 being non empty strict NORMSTR st
( the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the normF of b1 = Euclid_norm n )
proof end;
uniqueness
for b1, b2 being non empty strict NORMSTR st the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the normF of b1 = Euclid_norm n & the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the normF of b2 = Euclid_norm n holds
b1 = b2
;
end;

:: deftheorem Def4 defines REAL-NS REAL_NS1:def 4 :
for n being Nat
for b2 being non empty strict NORMSTR holds
( b2 = REAL-NS n iff ( the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the normF of b2 = Euclid_norm n ) );

registration
let n be non empty Nat;
cluster REAL-NS n -> non empty non trivial strict ;
coherence
not REAL-NS n is trivial
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 number 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 ;
coherence
( REAL-NS n is reflexive & REAL-NS n is discerning & REAL-NS n is RealNormSpace-like & REAL-NS n is vector-distributive & REAL-NS n is scalar-distributive & REAL-NS n is scalar-associative & REAL-NS n is scalar-unital & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )
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 Element of NAT st i in Seg n holds
0 <= x . i ) holds
( 0 <= Sum x & ( for i being Element of 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
abs (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
abs (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 Function of NAT,(REAL n);
let k be Nat;
:: original: .
redefine func f . k -> Element of REAL n;
coherence
f . k is Element of REAL n
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 Function of NAT,(REAL n) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Element of NAT st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Element of 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
REAL-NS n is complete
by Lm2;
end;

begin

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));
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y))
proof end;
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y)) ) & ( for x, y being Element of REAL n holds b2 . (x,y) = Sum (mlt (x,y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Euclid_scalar REAL_NS1:def 5 :
for n being Nat
for b2 being Function of [:(REAL n),(REAL n):],REAL holds
( b2 = Euclid_scalar n iff for x, y being Element of REAL n holds b2 . (x,y) = Sum (mlt (x,y)) );

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 );
existence
ex b1 being non empty strict UNITSTR st
( the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the scalar of b1 = Euclid_scalar n )
proof end;
uniqueness
for b1, b2 being non empty strict UNITSTR st the carrier of b1 = REAL n & 0. b1 = 0* n & the addF of b1 = Euclid_add n & the Mult of b1 = Euclid_mult n & the scalar of b1 = Euclid_scalar n & the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the scalar of b2 = Euclid_scalar n holds
b1 = b2
;
end;

:: deftheorem Def6 defines REAL-US REAL_NS1:def 6 :
for n being Nat
for b2 being non empty strict UNITSTR holds
( b2 = REAL-US n iff ( the carrier of b2 = REAL n & 0. b2 = 0* n & the addF of b2 = Euclid_add n & the Mult of b2 = Euclid_mult n & the scalar of b2 = Euclid_scalar n ) );

registration
let n be non empty Nat;
cluster REAL-US n -> non empty non trivial strict ;
coherence
not REAL-US n is trivial
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 ;
coherence
( REAL-US n is RealUnitarySpace-like & REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital & REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
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 ;
coherence
REAL-US n is complete
proof end;
end;