:: by Noboru Endou and Yasunari Shidama

::

:: Received December 28, 2005

:: Copyright (c) 2005-2018 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;

ex b_{1} being BinOp of (REAL n) st

for a, b being Element of REAL n holds b_{1} . (a,b) = a + b

for b_{1}, b_{2} being BinOp of (REAL n) st ( for a, b being Element of REAL n holds b_{1} . (a,b) = a + b ) & ( for a, b being Element of REAL n holds b_{2} . (a,b) = a + b ) holds

b_{1} = b_{2}

end;
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 for a, b being Element of REAL n holds it . (a,b) = a + b;

ex b

for a, b being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Euclid_add REAL_NS1:def 1 :

for n being Nat

for b_{2} being BinOp of (REAL n) holds

( b_{2} = Euclid_add n iff for a, b being Element of REAL n holds b_{2} . (a,b) = a + b );

for n being Nat

for b

( b

registration
end;

definition

let n be Nat;

ex b_{1} being Function of [:REAL,(REAL n):],(REAL n) st

for r being Real

for x being Element of REAL n holds b_{1} . (r,x) = r * x

for b_{1}, b_{2} being Function of [:REAL,(REAL n):],(REAL n) st ( for r being Real

for x being Element of REAL n holds b_{1} . (r,x) = r * x ) & ( for r being Real

for x being Element of REAL n holds b_{2} . (r,x) = r * x ) holds

b_{1} = b_{2}

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

existence for r being Real

for x being Element of REAL n holds it . (r,x) = r * x;

ex b

for r being Real

for x being Element of REAL n holds b

proof end;

uniqueness for b

for x being Element of REAL n holds b

for x being Element of REAL n holds b

b

proof end;

:: deftheorem Def2 defines Euclid_mult REAL_NS1:def 2 :

for n being Nat

for b_{2} being Function of [:REAL,(REAL n):],(REAL n) holds

( b_{2} = Euclid_mult n iff for r being Real

for x being Element of REAL n holds b_{2} . (r,x) = r * x );

for n being Nat

for b

( b

for x being Element of REAL n holds b

definition

let n be Nat;

ex b_{1} being Function of (REAL n),REAL st

for x being Element of REAL n holds b_{1} . x = |.x.|

for b_{1}, b_{2} being Function of (REAL n),REAL st ( for x being Element of REAL n holds b_{1} . x = |.x.| ) & ( for x being Element of REAL n holds b_{2} . x = |.x.| ) holds

b_{1} = b_{2}

end;
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 for x being Element of REAL n holds it . x = |.x.|;

ex b

for x being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Euclid_norm REAL_NS1:def 3 :

for n being Nat

for b_{2} being Function of (REAL n),REAL holds

( b_{2} = Euclid_norm n iff for x being Element of REAL n holds b_{2} . x = |.x.| );

for n being Nat

for b

( b

definition

let n be Nat;

ex b_{1} being non empty strict NORMSTR st

( the carrier of b_{1} = REAL n & 0. b_{1} = 0* n & the addF of b_{1} = Euclid_add n & the Mult of b_{1} = Euclid_mult n & the normF of b_{1} = Euclid_norm n )

for b_{1}, b_{2} being non empty strict NORMSTR st the carrier of b_{1} = REAL n & 0. b_{1} = 0* n & the addF of b_{1} = Euclid_add n & the Mult of b_{1} = Euclid_mult n & the normF of b_{1} = Euclid_norm n & the carrier of b_{2} = REAL n & 0. b_{2} = 0* n & the addF of b_{2} = Euclid_add n & the Mult of b_{2} = Euclid_mult n & the normF of b_{2} = Euclid_norm n holds

b_{1} = b_{2}
;

end;
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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

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

for n being Nat

for b_{2} being non empty strict NORMSTR holds

( b_{2} = REAL-NS n iff ( the carrier of b_{2} = REAL n & 0. b_{2} = 0* n & the addF of b_{2} = Euclid_add n & the Mult of b_{2} = Euclid_mult n & the normF of b_{2} = Euclid_norm n ) );

for n being Nat

for b

( b

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

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

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

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;

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

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

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

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

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

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

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

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)

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

f . k is Element of REAL n

end;
let f be sequence of (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;

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

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

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;

definition

let n be Nat;

ex b_{1} being Function of [:(REAL n),(REAL n):],REAL st

for x, y being Element of REAL n holds b_{1} . (x,y) = Sum (mlt (x,y))

for b_{1}, b_{2} being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b_{1} . (x,y) = Sum (mlt (x,y)) ) & ( for x, y being Element of REAL n holds b_{2} . (x,y) = Sum (mlt (x,y)) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of REAL n holds it . (x,y) = Sum (mlt (x,y));

ex b

for x, y being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines Euclid_scalar REAL_NS1:def 5 :

for n being Nat

for b_{2} being Function of [:(REAL n),(REAL n):],REAL holds

( b_{2} = Euclid_scalar n iff for x, y being Element of REAL n holds b_{2} . (x,y) = Sum (mlt (x,y)) );

for n being Nat

for b

( b

definition

let n be Nat;

ex b_{1} being non empty strict UNITSTR st

( the carrier of b_{1} = REAL n & 0. b_{1} = 0* n & the addF of b_{1} = Euclid_add n & the Mult of b_{1} = Euclid_mult n & the scalar of b_{1} = Euclid_scalar n )

for b_{1}, b_{2} being non empty strict UNITSTR st the carrier of b_{1} = REAL n & 0. b_{1} = 0* n & the addF of b_{1} = Euclid_add n & the Mult of b_{1} = Euclid_mult n & the scalar of b_{1} = Euclid_scalar n & the carrier of b_{2} = REAL n & 0. b_{2} = 0* n & the addF of b_{2} = Euclid_add n & the Mult of b_{2} = Euclid_mult n & the scalar of b_{2} = Euclid_scalar n holds

b_{1} = b_{2}
;

end;
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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

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

for n being Nat

for b_{2} being non empty strict UNITSTR holds

( b_{2} = REAL-US n iff ( the carrier of b_{2} = REAL n & 0. b_{2} = 0* n & the addF of b_{2} = Euclid_add n & the Mult of b_{2} = Euclid_mult n & the scalar of b_{2} = Euclid_scalar n ) );

for n being Nat

for b

( b

registration

let n be Nat;

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

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

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 )

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

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

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

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

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

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;