:: HAUSDORF semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let r be real number ;
:: original: {
redefine func {r} -> Subset of REAL ;
coherence
{r} is Subset of REAL
proof end;
end;

registration
let M be non empty MetrSpace;
cluster TopSpaceMetr M -> being_T2 ;
coherence
TopSpaceMetr M is being_T2
by PCOMPS_1:38;
end;

theorem Th1: :: HAUSDORF:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st x >= 0 & y >= 0 & max x,y = 0 holds
x = 0
proof end;

theorem Th2: :: HAUSDORF:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for x being Point of M holds (dist x) . x = 0
proof end;

theorem Th3: :: HAUSDORF:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for x being Point of M st x in P holds
0 in (dist x) .: P
proof end;

theorem Th4: :: HAUSDORF:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for x being Point of M
for y being real number st y in (dist x) .: P holds
y >= 0
proof end;

theorem Th5: :: HAUSDORF:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for x being set st x in P holds
(dist_min P) . x = 0
proof end;

theorem Th6: :: HAUSDORF:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for p being Point of M
for q being Point of (TopSpaceMetr M)
for r being real number st p = q & r > 0 holds
Ball p,r is a_neighborhood of q
proof end;

theorem Th7: :: HAUSDORF:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for A being Subset of (TopSpaceMetr M)
for p being Point of M holds
( p in Cl A iff for r being real number st r > 0 holds
Ball p,r meets A )
proof end;

theorem Th8: :: HAUSDORF:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for p being Point of M
for A being Subset of (TopSpaceMetr M) holds
( p in Cl A iff for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r ) )
proof end;

theorem Th9: :: HAUSDORF:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M holds
( (dist_min P) . x = 0 iff for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist x,p < r ) )
proof end;

theorem Th10: :: HAUSDORF:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M holds
( x in Cl P iff (dist_min P) . x = 0 )
proof end;

theorem Th11: :: HAUSDORF:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty closed Subset of (TopSpaceMetr M)
for x being Point of M holds
( x in P iff (dist_min P) . x = 0 )
proof end;

theorem Th12: :: HAUSDORF:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Subset of R^1 ex X being non empty Subset of REAL st
( A = X & lower_bound A = inf X )
proof end;

theorem Th13: :: HAUSDORF:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Subset of R^1 ex X being non empty Subset of REAL st
( A = X & upper_bound A = sup X )
proof end;

theorem Th14: :: HAUSDORF:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 holds
X is bounded_below
proof end;

theorem Th15: :: HAUSDORF:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M st y in P holds
(dist_min P) . x <= dist x,y
proof end;

theorem Th16: :: HAUSDORF:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for r being real number
for x being Point of M st ( for y being Point of M st y in P holds
dist x,y >= r ) holds
(dist_min P) . x >= r
proof end;

theorem Th17: :: HAUSDORF:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M holds (dist_min P) . x <= (dist x,y) + ((dist_min P) . y)
proof end;

theorem Th18: :: HAUSDORF:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for Q being non empty Subset of M st P = Q holds
(TopSpaceMetr M) | P = TopSpaceMetr (M | Q)
proof end;

theorem Th19: :: HAUSDORF:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for A being Subset of M
for B being non empty Subset of M
for C being Subset of (M | B) st A c= B & A = C & C is bounded holds
A is bounded
proof end;

theorem :: HAUSDORF:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for B being Subset of M
for A being Subset of (TopSpaceMetr M) st A = B & A is compact holds
B is bounded
proof end;

theorem Th21: :: HAUSDORF:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M ex w being Point of M st
( w in P & (dist_min P) . z <= dist w,z )
proof end;

registration
let M be non empty MetrSpace;
let x be Point of M;
cluster dist x -> continuous ;
coherence
dist x is continuous
by WEIERSTR:22;
end;

registration
let M be non empty MetrSpace;
let X be non empty compact Subset of (TopSpaceMetr M);
cluster dist_max X -> continuous ;
coherence
dist_max X is continuous
by WEIERSTR:30;
cluster dist_min X -> continuous ;
coherence
dist_min X is continuous
by WEIERSTR:33;
end;

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
proof end;

theorem Th22: :: HAUSDORF:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M st y in P & P is compact holds
(dist_max P) . x >= dist x,y
proof end;

theorem :: HAUSDORF:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact holds
ex w being Point of M st
( w in P & (dist_max P) . z >= dist w,z )
proof end;

theorem Th24: :: HAUSDORF:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact & Q is compact & z in Q holds
(dist_min P) . z <= max_dist_max P,Q
proof end;

theorem Th25: :: HAUSDORF:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact & Q is compact & z in Q holds
(dist_max P) . z <= max_dist_max P,Q
proof end;

theorem :: HAUSDORF:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M)
for X being Subset of REAL st X = (dist_max P) .: Q & P is compact & Q is compact holds
X is bounded_above
proof end;

theorem Th27: :: HAUSDORF:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M)
for X being Subset of REAL st X = (dist_min P) .: Q & P is compact & Q is compact holds
X is bounded_above
proof end;

theorem :: HAUSDORF:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact holds
(dist_min P) . z <= (dist_max P) . z
proof end;

theorem Th29: :: HAUSDORF:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0}
proof end;

theorem Th30: :: HAUSDORF:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
max_dist_min P,Q >= 0
proof end;

theorem Th31: :: HAUSDORF:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds max_dist_min P,P = 0
proof end;

theorem :: HAUSDORF:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
min_dist_max P,Q >= 0
proof end;

theorem Th33: :: HAUSDORF:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for Q, R being non empty Subset of (TopSpaceMetr M)
for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= max_dist_min R,Q
proof end;

definition
let M be non empty MetrSpace;
let P, Q be Subset of (TopSpaceMetr M);
func HausDist P,Q -> Real equals :: HAUSDORF:def 1
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: :: HAUSDORF:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for Q, R being non empty Subset of (TopSpaceMetr M)
for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= HausDist Q,R
proof end;

theorem Th35: :: HAUSDORF:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds
max_dist_min P,R <= (HausDist P,Q) + (HausDist Q,R)
proof end;

theorem Th36: :: HAUSDORF:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds
max_dist_min R,P <= (HausDist P,Q) + (HausDist Q,R)
proof end;

theorem Th37: :: HAUSDORF:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
HausDist P,Q >= 0
proof end;

theorem Th38: :: HAUSDORF:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds HausDist P,P = 0 by Th31;

theorem Th39: :: HAUSDORF:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & HausDist P,Q = 0 holds
P = Q
proof end;

theorem Th40: :: HAUSDORF:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds
HausDist P,R <= (HausDist P,Q) + (HausDist Q,R)
proof end;

definition
let n be Nat;
let P, Q be Subset of (TOP-REAL n);
func max_dist_min P,Q -> Real means :: HAUSDORF:def 2
ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & it = max_dist_min P',Q' );
existence
ex b1 being Real ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = max_dist_min P',Q' )
proof end;
uniqueness
for b1, b2 being Real st ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = max_dist_min P',Q' ) & ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b2 = max_dist_min P',Q' ) holds
b1 = b2
;
end;

:: deftheorem defines max_dist_min HAUSDORF:def 2 :
for n being Nat
for P, Q being Subset of (TOP-REAL n)
for b4 being Real holds
( b4 = max_dist_min P,Q iff ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b4 = max_dist_min P',Q' ) );

definition
let n be Nat;
let P, Q be Subset of (TOP-REAL n);
func HausDist P,Q -> Real means :Def3: :: HAUSDORF:def 3
ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & it = HausDist P',Q' );
existence
ex b1 being Real ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = HausDist P',Q' )
proof end;
uniqueness
for b1, b2 being Real st ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = HausDist P',Q' ) & ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b2 = HausDist P',Q' ) holds
b1 = b2
;
commutativity
for b1 being Real
for P, Q being Subset of (TOP-REAL n) st ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = HausDist P',Q' ) holds
ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( Q = P' & P = Q' & b1 = HausDist P',Q' )
;
end;

:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :
for n being Nat
for P, Q being Subset of (TOP-REAL n)
for b4 being Real holds
( b4 = HausDist P,Q iff ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b4 = HausDist P',Q' ) );

theorem :: HAUSDORF:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact holds
HausDist P,Q >= 0
proof end;

theorem :: HAUSDORF:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for P being non empty Subset of (TOP-REAL n) holds HausDist P,P = 0
proof end;

theorem :: HAUSDORF:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact & HausDist P,Q = 0 holds
P = Q
proof end;

theorem :: HAUSDORF:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for P, Q, R being non empty Subset of (TOP-REAL n) st P is compact & Q is compact & R is compact holds
HausDist P,R <= (HausDist P,Q) + (HausDist Q,R)
proof end;