begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
Lm1:
for M being non empty MetrSpace
for P being non empty Subset of
for x being Point of
for X being Subset of st X = (dist x) .: P & P is compact holds
X is bounded_above
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem Th33:
begin
definition
let M be non
empty MetrSpace;
let P,
Q be
Subset of ;
func HausDist P,
Q -> Real equals
max (max_dist_min P,Q),
(max_dist_min Q,P);
coherence
max (max_dist_min P,Q),(max_dist_min Q,P) is Real
;
commutativity
for b1 being Real
for P, Q being Subset of st b1 = max (max_dist_min P,Q),(max_dist_min Q,P) holds
b1 = max (max_dist_min Q,P),(max_dist_min P,Q)
;
end;
:: deftheorem defines HausDist HAUSDORF:def 1 :
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of ;
func max_dist_min P,
Q -> Real means
ex
P',
Q' being
Subset of st
(
P = P' &
Q = Q' &
it = max_dist_min P',
Q' );
existence
ex b1 being Real ex P', Q' being Subset of st
( P = P' & Q = Q' & b1 = max_dist_min P',Q' )
uniqueness
for b1, b2 being Real st ex P', Q' being Subset of st
( P = P' & Q = Q' & b1 = max_dist_min P',Q' ) & ex P', Q' being Subset of st
( P = P' & Q = Q' & b2 = max_dist_min P',Q' ) holds
b1 = b2
;
end;
:: deftheorem defines max_dist_min HAUSDORF:def 2 :
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of ;
func HausDist P,
Q -> Real means :
Def3:
ex
P',
Q' being
Subset of st
(
P = P' &
Q = Q' &
it = HausDist P',
Q' );
existence
ex b1 being Real ex P', Q' being Subset of st
( P = P' & Q = Q' & b1 = HausDist P',Q' )
uniqueness
for b1, b2 being Real st ex P', Q' being Subset of st
( P = P' & Q = Q' & b1 = HausDist P',Q' ) & ex P', Q' being Subset of st
( P = P' & Q = Q' & b2 = HausDist P',Q' ) holds
b1 = b2
;
commutativity
for b1 being Real
for P, Q being Subset of st ex P', Q' being Subset of st
( P = P' & Q = Q' & b1 = HausDist P',Q' ) holds
ex P', Q' being Subset of st
( Q = P' & P = Q' & b1 = HausDist P',Q' )
;
end;
:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :
theorem
theorem
theorem
theorem