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