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 (TopSpaceMetr M)
for x being Point of M
for X being Subset of REAL 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
(TopSpaceMetr M);
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 (TopSpaceMetr M) 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 :
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds HausDist P,Q = max (max_dist_min P,Q),(max_dist_min Q,P);
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of
(TOP-REAL n);
func max_dist_min P,
Q -> Real means
ex
P9,
Q9 being
Subset of
(TopSpaceMetr (Euclid n)) st
(
P = P9 &
Q = Q9 &
it = max_dist_min P9,
Q9 );
existence
ex b1 being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = max_dist_min P9,Q9 )
uniqueness
for b1, b2 being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = max_dist_min P9,Q9 ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b2 = max_dist_min P9,Q9 ) holds
b1 = b2
;
end;
:: deftheorem defines max_dist_min HAUSDORF:def 2 :
for n being Element of NAT
for P, Q being Subset of (TOP-REAL n)
for b4 being Real holds
( b4 = max_dist_min P,Q iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b4 = max_dist_min P9,Q9 ) );
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of
(TOP-REAL n);
func HausDist P,
Q -> Real means :
Def3:
ex
P9,
Q9 being
Subset of
(TopSpaceMetr (Euclid n)) st
(
P = P9 &
Q = Q9 &
it = HausDist P9,
Q9 );
existence
ex b1 being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = HausDist P9,Q9 )
uniqueness
for b1, b2 being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = HausDist P9,Q9 ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b2 = HausDist P9,Q9 ) holds
b1 = b2
;
commutativity
for b1 being Real
for P, Q being Subset of (TOP-REAL n) st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = HausDist P9,Q9 ) holds
ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( Q = P9 & P = Q9 & b1 = HausDist P9,Q9 )
;
end;
:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :
for n being Element of NAT
for P, Q being Subset of (TOP-REAL n)
for b4 being Real holds
( b4 = HausDist P,Q iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b4 = HausDist P9,Q9 ) );
theorem
theorem
theorem
theorem