:: Completeness of the Real {E}uclidean Space
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 28, 2005
:: Copyright (c) 2005 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 )
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:
:: 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
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: :: REAL_NS1:1
theorem Th2: :: REAL_NS1:2
theorem Th3: :: REAL_NS1:3
theorem Th4: :: REAL_NS1:4
theorem Th5: :: REAL_NS1:5
theorem Th6: :: REAL_NS1:6
theorem Th7: :: REAL_NS1:7
theorem Th8: :: REAL_NS1:8
theorem Th9: :: REAL_NS1:9
theorem Th10: :: REAL_NS1:10
theorem Th11: :: REAL_NS1:11
theorem Th12: :: REAL_NS1:12
Lm3:
for n being Element of NAT holds REAL-NS n is RealBanachSpace
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)
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: :: REAL_NS1:13
theorem :: REAL_NS1:14
theorem Th15: :: REAL_NS1:15
theorem Th16: :: REAL_NS1:16
theorem :: REAL_NS1:17
theorem Th18: :: REAL_NS1:18
Lm4:
for n being Element of NAT holds REAL-US n is Hilbert