begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem
theorem
theorem Th20:
theorem
theorem Th22:
theorem
canceled;
theorem Th24:
begin
theorem Th25:
theorem
begin
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
for
r being
Real for
s,
p,
q being
Point of st
s = ((1 - r) * p) + (r * q) &
s <> q &
r <= 1 holds
r < 1
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th61:
theorem
theorem
theorem
Lm1:
for M being non empty MetrSpace
for z being Point of
for r being real number
for A being Subset of st A = cl_Ball z,r holds
A ` is open
theorem Th65:
theorem
theorem Th67:
theorem Th68:
theorem
theorem
theorem Th71:
theorem
theorem Th73:
theorem
theorem
canceled;
theorem Th76:
begin
theorem Th77:
theorem Th78:
Lm2:
R^1 = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6, TOPMETR:def 7;
theorem Th79:
theorem
theorem Th81:
theorem
theorem Th83:
theorem Th84:
theorem Th85:
theorem
begin
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
theorem
theorem
theorem
theorem
theorem Th98:
theorem
begin
definition
let n be
Element of
NAT ;
let a,
b be
Point of ;
func dist a,
b -> Real means :
Def1:
ex
p,
q being
Point of st
(
p = a &
q = b &
it = dist p,
q );
existence
ex b1 being Real ex p, q being Point of st
( p = a & q = b & b1 = dist p,q )
uniqueness
for b1, b2 being Real st ex p, q being Point of st
( p = a & q = b & b1 = dist p,q ) & ex p, q being Point of st
( p = a & q = b & b2 = dist p,q ) holds
b1 = b2
;
commutativity
for b1 being Real
for a, b being Point of st ex p, q being Point of st
( p = a & q = b & b1 = dist p,q ) holds
ex p, q being Point of st
( p = b & q = a & b1 = dist p,q )
;
end;
:: deftheorem Def1 defines dist TOPREAL6:def 1 :
theorem Th100:
theorem Th101:
theorem
theorem
theorem