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 )
Lm2:
for n being Nat ex f being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds f . (r,x) = r * x
:: 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 );
definition
let n be
Nat;
func Euclid_mult n -> Function of
[:REAL,(REAL n):],
(REAL n) means :
Def2:
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
by Lm2;
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
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 );
:: 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.| );
:: 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 ) );
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
Lm3:
for n being Nat holds REAL-NS n is RealBanachSpace
begin
definition
let n be
Nat;
func Euclid_scalar n -> Function of
[:(REAL n),(REAL n):],
REAL means :
Def5:
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))
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
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)) );
:: 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 ) );
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18: