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:
for
n being
Element of
NAT for
a being
Real for
x1,
y1 being
Point of
for
x2,
y2 being
Point of st
x1 = x2 &
y1 = y2 holds
(
x1 + y1 = x2 + y2 &
- x1 = - x2 &
a * x1 = a * x2 )
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
Lm4:
for n being Element of NAT holds REAL-US n is Hilbert