begin
:: deftheorem defines REAL EUCLID:def 1 :
:: deftheorem Def2 defines absreal EUCLID:def 2 :
:: deftheorem defines abs EUCLID:def 3 :
:: deftheorem defines 0* EUCLID:def 4 :
:: deftheorem defines |. EUCLID:def 5 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
Lm1:
for f being real-valued FinSequence holds f is FinSequence of REAL
Lm2:
for f being real-valued FinSequence holds f is Element of REAL (len f)
theorem
theorem Th8:
theorem Th9:
theorem Th10:
Lm3:
for f being real-valued FinSequence holds sqr (abs f) = sqr f
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
theorem
theorem Th19:
theorem
theorem Th21:
theorem Th22:
definition
let n be
Nat;
func Pitag_dist n -> Function of
[:(REAL n),(REAL n):],
REAL means :
Def6:
for
x,
y being
Element of
REAL n holds
it . x,
y = |.(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 = |.(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 = |.(x - y).| ) & ( for x, y being Element of REAL n holds b2 . x,y = |.(x - y).| ) holds
b1 = b2
end;
:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :
theorem
theorem Th24:
:: deftheorem defines Euclid EUCLID:def 7 :
definition
let n be
Nat;
func TOP-REAL n -> strict RLTopStruct means :
Def8:
(
TopStruct(# the
carrier of
it,the
topology of
it #)
= TopSpaceMetr (Euclid n) &
RLSStruct(# the
carrier of
it,the
ZeroF of
it,the
addF of
it,the
Mult of
it #)
= RealVectSpace (Seg n) );
existence
ex b1 being strict RLTopStruct st
( TopStruct(# the carrier of b1,the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1,the ZeroF of b1,the addF of b1,the Mult of b1 #) = RealVectSpace (Seg n) )
uniqueness
for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1,the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1,the ZeroF of b1,the addF of b1,the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2,the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2,the ZeroF of b2,the addF of b2,the Mult of b2 #) = RealVectSpace (Seg n) holds
b1 = b2
;
end;
:: deftheorem Def8 defines TOP-REAL EUCLID:def 8 :
theorem Th25:
theorem Th26:
theorem Th27:
Lm4:
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
Lm5:
for n being Nat
for p being Point of (TOP-REAL n)
for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem EUCLID:def 9 :
canceled;
:: deftheorem EUCLID:def 10 :
canceled;
:: deftheorem EUCLID:def 11 :
canceled;
:: deftheorem EUCLID:def 12 :
canceled;
:: deftheorem EUCLID:def 13 :
canceled;
:: deftheorem defines `1 EUCLID:def 14 :
:: deftheorem defines `2 EUCLID:def 15 :
theorem
theorem Th57:
theorem
theorem Th59:
theorem
theorem Th61:
theorem
theorem Th63:
theorem
theorem Th65:
theorem
theorem
theorem
theorem
theorem Th70:
theorem
theorem
theorem
theorem
theorem