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 :
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 :
:: deftheorem Def3 defines Euclid_norm REAL_NS1:def 3 :
:: deftheorem Def4 defines REAL-NS REAL_NS1:def 4 :
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 Element of 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 :
:: deftheorem Def6 defines REAL-US REAL_NS1:def 6 :
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
Lm4:
for n being Element of NAT holds REAL-US n is Hilbert