:: HAUSDORF semantic presentation

begin

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

theorem Th1: :: HAUSDORF:1
for x, y being real number st x >= 0 & max (x,y) = 0 holds
x = 0
proof
let x, y be real number ; ::_thesis: ( x >= 0 & max (x,y) = 0 implies x = 0 )
assume that
A1: x >= 0 and
A2: max (x,y) = 0 ; ::_thesis: x = 0
percases ( max (x,y) = x or max (x,y) = y ) by XXREAL_0:16;
suppose max (x,y) = x ; ::_thesis: x = 0
hence  x = 0 by A2; ::_thesis: verum
end;
supposeA3: max (x,y) = y ; ::_thesis: x = 0
then  x <= y by XXREAL_0:25;
hence  x = 0 by A1, A2, A3, XXREAL_0:1; ::_thesis: verum
end;
end;
end;

theorem Th2: :: HAUSDORF:2
for M being non empty MetrSpace
for x being Point of M holds (dist x) . x = 0
proof
let M be non empty MetrSpace; ::_thesis: for x being Point of M holds (dist x) . x = 0
let x be Point of M; ::_thesis: (dist x) . x = 0
(dist x) . x = dist (x,x) by WEIERSTR:def_4
.= 0 by METRIC_1:1 ;
hence  (dist x) . x = 0 ; ::_thesis: verum
end;

theorem Th3: :: HAUSDORF:3
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
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M)
for x being Point of M st x in P holds
0 in (dist x) .: P
let P be Subset of (TopSpaceMetr M); ::_thesis: for x being Point of M st x in P holds
0 in (dist x) .: P
let x be Point of M; ::_thesis: ( x in P implies 0 in (dist x) .: P )
A1: dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
assume  x in P ; ::_thesis: 0 in (dist x) .: P
then  (dist x) . x in (dist x) .: P by A1, FUNCT_1:def_6;
hence  0 in (dist x) .: P by Th2; ::_thesis: verum
end;

theorem Th4: :: HAUSDORF:4
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
let M be non empty MetrSpace; ::_thesis: 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
let P be Subset of (TopSpaceMetr M); ::_thesis: for x being Point of M
for y being real number st y in (dist x) .: P holds
y >= 0
let x be Point of M; ::_thesis: for y being real number st y in (dist x) .: P holds
y >= 0
let y be real number ; ::_thesis: ( y in (dist x) .: P implies y >= 0 )
assume  y in (dist x) .: P ; ::_thesis: y >= 0
then consider z being set  such that
 z in dom (dist x) and
A1: z in P and
A2: y = (dist x) . z by FUNCT_1:def_6;
reconsider z9 = z as Point of M by A1, TOPMETR:12;
 y = dist (x,z9) by A2, WEIERSTR:def_4;
hence  y >= 0 by METRIC_1:5; ::_thesis: verum
end;

theorem Th5: :: HAUSDORF:5
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
let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M)
for x being set st x in P holds
(dist_min P) . x = 0
let P be Subset of (TopSpaceMetr M); ::_thesis: for x being set st x in P holds
(dist_min P) . x = 0
let x be set ; ::_thesis: ( x in P implies (dist_min P) . x = 0 )
assume A1: x in P ; ::_thesis: (dist_min P) . x = 0
then reconsider x = x as Point of M by TOPMETR:12;
set X = (dist x) .: P;
reconsider X = (dist x) .: P as non empty Subset of REAL by A1, TOPMETR:17;
lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def_3
.= lower_bound X by WEIERSTR:def_1 ;
then A2: (dist_min P) . x = lower_bound X by WEIERSTR:def_6;
A3: for p being real number st p in X holds
p >= 0 by Th4;
 for q being real number st ( for p being real number st p in X holds
p >= q ) holds
0 >= q by A1, Th3;
hence  (dist_min P) . x = 0 by A2, A3, SEQ_4:44; ::_thesis: verum
end;

theorem Th6: :: HAUSDORF:6
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
let M be non empty MetrSpace; ::_thesis: 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 ) )
let p be Point of M; ::_thesis: 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 ) )
let A be Subset of (TopSpaceMetr M); ::_thesis: ( 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 ) )
hereby  ::_thesis: ( ( for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist (p,q) < r ) ) implies p in Cl A )
assume A1: p in Cl A ; ::_thesis: for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist (p,q) < r )
let r be real number ; ::_thesis: ( r > 0 implies ex q being Point of M st
( q in A & dist (p,q) < r ) )
assume  r > 0 ; ::_thesis: ex q being Point of M st
( q in A & dist (p,q) < r )
then  Ball (p,r) meets A by A1, GOBOARD6:92;
then consider x being set  such that
A2: x in Ball (p,r) and
A3: x in A by XBOOLE_0:3;
reconsider q = x as Point of M by A2;
take q = q; ::_thesis: ( q in A & dist (p,q) < r )
thus  q in A by A3; ::_thesis: dist (p,q) < r
thus  dist (p,q) < r by A2, METRIC_1:11; ::_thesis: verum
end;
assume A4: for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist (p,q) < r ) ; ::_thesis: p in Cl A
 for r being real number st r > 0 holds
Ball (p,r) meets A
proof
let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A )
assume  r > 0 ; ::_thesis: Ball (p,r) meets A
then consider q being Point of M such that
A5: q in A and
A6: dist (p,q) < r by A4;
 q in Ball (p,r) by A6, METRIC_1:11;
hence  Ball (p,r) meets A by A5, XBOOLE_0:3; ::_thesis: verum
end;
hence  p in Cl A by GOBOARD6:92; ::_thesis: verum
end;

theorem Th7: :: HAUSDORF:7
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
let M be non empty MetrSpace; ::_thesis: 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 ) )
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: 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 ) )
let x be Point of M; ::_thesis: ( (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 ) )
reconsider X = (dist x) .: P as non empty Subset of REAL by TOPMETR:17;
hereby  ::_thesis: ( ( for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < r ) ) implies (dist_min P) . x = 0 )
assume A1: (dist_min P) . x = 0 ; ::_thesis: for r being real number st r > 0 holds
ex p being Point of M st
( p in P & not dist (x,p) >= r )
let r be real number ; ::_thesis: ( r > 0 implies ex p being Point of M st
( p in P & not dist (x,p) >= r ) )
assume A2: r > 0 ; ::_thesis: ex p being Point of M st
( p in P & not dist (x,p) >= r )
assume A3: for p being Point of M st p in P holds
dist (x,p) >= r ; ::_thesis: contradiction
 for p being real number st p in X holds
p >= r
proof
let p be real number ; ::_thesis: ( p in X implies p >= r )
assume  p in X ; ::_thesis: p >= r
then consider y being set  such that
A4: y in dom (dist x) and
A5: y in P and
A6: p = (dist x) . y by FUNCT_1:def_6;
reconsider z = y as Point of M by A4, TOPMETR:12;
 dist (x,z) >= r by A3, A5;
hence  p >= r by A6, WEIERSTR:def_4; ::_thesis: verum
end;
then A7: lower_bound X >= r by SEQ_4:43;
lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def_3
.= lower_bound X by WEIERSTR:def_1 ;
hence  contradiction by A1, A2, A7, WEIERSTR:def_6; ::_thesis: verum
end;
A8: for p being real number st p in X holds
p >= 0
proof
let p be real number ; ::_thesis: ( p in X implies p >= 0 )
assume  p in X ; ::_thesis: p >= 0
then consider y being set  such that
A9: y in dom (dist x) and
 y in P and
A10: p = (dist x) . y by FUNCT_1:def_6;
reconsider z = y as Point of M by A9, TOPMETR:12;
 dist (x,z) >= 0 by METRIC_1:5;
hence  p >= 0 by A10, WEIERSTR:def_4; ::_thesis: verum
end;
assume A11: for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < r ) ; ::_thesis: (dist_min P) . x = 0
A12: for q being real number st ( for p being real number st p in X holds
p >= q ) holds
0 >= q
proof
let q be real number ; ::_thesis: ( ( for p being real number st p in X holds
p >= q ) implies 0 >= q )
assume A13: for z being real number st z in X holds
z >= q ; ::_thesis: 0 >= q
assume  0 < q ; ::_thesis: contradiction
then consider p being Point of M such that
A14: p in P and
A15: dist (x,p) < q by A11;
set z = (dist x) . p;
 p in the carrier of (TopSpaceMetr M) by A14;
then  p in dom (dist x) by FUNCT_2:def_1;
then A16: (dist x) . p in X by A14, FUNCT_1:def_6;
 (dist x) . p < q by A15, WEIERSTR:def_4;
hence  contradiction by A13, A16; ::_thesis: verum
end;
lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def_3
.= lower_bound X by WEIERSTR:def_1 ;
then  lower_bound ((dist x) .: P) = 0 by A8, A12, SEQ_4:44;
hence  (dist_min P) . x = 0 by WEIERSTR:def_6; ::_thesis: verum
end;

theorem Th8: :: HAUSDORF:8
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
let M be non empty MetrSpace; ::_thesis: 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 )
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for x being Point of M holds
( x in Cl P iff (dist_min P) . x = 0 )
let x be Point of M; ::_thesis: ( x in Cl P iff (dist_min P) . x = 0 )
hereby  ::_thesis: ( (dist_min P) . x = 0 implies x in Cl P )
assume  x in Cl P ; ::_thesis: (dist_min P) . x = 0
then  for a being real number st a > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < a ) by Th6;
hence  (dist_min P) . x = 0 by Th7; ::_thesis: verum
end;
assume  (dist_min P) . x = 0 ; ::_thesis: x in Cl P
then  for a being real number st a > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < a ) by Th7;
hence  x in Cl P by Th6; ::_thesis: verum
end;

theorem Th9: :: HAUSDORF:9
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
let M be non empty MetrSpace; ::_thesis: 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 )
let P be non empty closed Subset of (TopSpaceMetr M); ::_thesis: for x being Point of M holds
( x in P iff (dist_min P) . x = 0 )
let x be Point of M; ::_thesis: ( x in P iff (dist_min P) . x = 0 )
 P = Cl P by PRE_TOPC:22;
hence  ( x in P iff (dist_min P) . x = 0 ) by Th8; ::_thesis: verum
end;

theorem Th10: :: HAUSDORF:10
for A being non empty Subset of R^1 ex X being non empty Subset of REAL st
( A = X & lower_bound A = lower_bound X )
proof
let A be non empty Subset of R^1; ::_thesis: ex X being non empty Subset of REAL st
( A = X & lower_bound A = lower_bound X )
reconsider X = A as non empty Subset of REAL by TOPMETR:17;
take  X ; ::_thesis: ( A = X & lower_bound A = lower_bound X )
lower_bound A = lower_bound ([#] A) by WEIERSTR:def_3
.= lower_bound X by WEIERSTR:def_1 ;
hence  ( A = X & lower_bound A = lower_bound X ) ; ::_thesis: verum
end;

theorem Th11: :: HAUSDORF:11
for A being non empty Subset of R^1 ex X being non empty Subset of REAL st
( A = X & upper_bound A = upper_bound X )
proof
let A be non empty Subset of R^1; ::_thesis: ex X being non empty Subset of REAL st
( A = X & upper_bound A = upper_bound X )
reconsider X = A as non empty Subset of REAL by TOPMETR:17;
take  X ; ::_thesis: ( A = X & upper_bound A = upper_bound X )
upper_bound A = upper_bound ([#] A) by WEIERSTR:def_2
.= upper_bound X by WEIERSTR:def_1 ;
hence  ( A = X & upper_bound A = upper_bound X ) ; ::_thesis: verum
end;

theorem Th12: :: HAUSDORF:12
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
let M be non empty MetrSpace; ::_thesis: 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
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for x being Point of M
for X being Subset of REAL st X = (dist x) .: P holds
X is bounded_below
let x be Point of M; ::_thesis: for X being Subset of REAL st X = (dist x) .: P holds
X is bounded_below
let X be Subset of REAL; ::_thesis: ( X = (dist x) .: P implies X is bounded_below )
assume A1: X = (dist x) .: P ; ::_thesis: X is bounded_below
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in X or 0 <= y )
thus  ( y in X implies 0 <= y ) by A1, Th4; ::_thesis: verum
end;

theorem Th13: :: HAUSDORF:13
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
let M be non empty MetrSpace; ::_thesis: 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)
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for x, y being Point of M st y in P holds
(dist_min P) . x <= dist (x,y)
let x, y be Point of M; ::_thesis: ( y in P implies (dist_min P) . x <= dist (x,y) )
A1: ( dom (dist x) = the carrier of (TopSpaceMetr M) & dist (x,y) = (dist x) . y ) by FUNCT_2:def_1, WEIERSTR:def_4;
consider X being non empty Subset of REAL such that
A2: X = (dist x) .: P and
A3: lower_bound ((dist x) .: P) = lower_bound X by Th10;
assume  y in P ; ::_thesis: (dist_min P) . x <= dist (x,y)
then A4: dist (x,y) in X by A2, A1, FUNCT_1:def_6;
 ( (dist_min P) . x = lower_bound X & X is bounded_below ) by A2, A3, Th12, WEIERSTR:def_6;
hence  (dist_min P) . x <= dist (x,y) by A4, SEQ_4:def_2; ::_thesis: verum
end;

theorem Th14: :: HAUSDORF:14
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
let M be non empty MetrSpace; ::_thesis: 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
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: 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
let r be real number ; ::_thesis: 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
let x be Point of M; ::_thesis: ( ( for y being Point of M st y in P holds
dist (x,y) >= r ) implies (dist_min P) . x >= r )
consider X being non empty Subset of REAL such that
A1: X = (dist x) .: P and
A2: lower_bound ((dist x) .: P) = lower_bound X by Th10;
assume A3: for y being Point of M st y in P holds
dist (x,y) >= r ; ::_thesis: (dist_min P) . x >= r
 for p being real number st p in X holds
p >= r
proof
let p be real number ; ::_thesis: ( p in X implies p >= r )
assume  p in X ; ::_thesis: p >= r
then consider y being set  such that
A4: y in dom (dist x) and
A5: y in P and
A6: (dist x) . y = p by A1, FUNCT_1:def_6;
reconsider y = y as Point of M by A4, TOPMETR:12;
 p = dist (x,y) by A6, WEIERSTR:def_4;
hence  p >= r by A3, A5; ::_thesis: verum
end;
then  lower_bound X >= r by SEQ_4:43;
hence  (dist_min P) . x >= r by A2, WEIERSTR:def_6; ::_thesis: verum
end;

theorem Th15: :: HAUSDORF:15
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
let M be non empty MetrSpace; ::_thesis: 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)
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for x, y being Point of M holds (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
let x, y be Point of M; ::_thesis: (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
now__::_thesis:_for_z_being_Point_of_M_st_z_in_P_holds_
dist_(y,z)_>=_((dist_min_P)_._x)_-_(dist_(x,y))
let z be Point of M; ::_thesis: ( z in P implies dist (y,z) >= ((dist_min P) . x) - (dist (x,y)) )
assume  z in P ; ::_thesis: dist (y,z) >= ((dist_min P) . x) - (dist (x,y))
then  (dist_min P) . x <= dist (x,z) by Th13;
then A1: (dist (x,z)) - (dist (x,y)) >= ((dist_min P) . x) - (dist (x,y)) by XREAL_1:13;
 dist (x,z) <= (dist (x,y)) + (dist (y,z)) by METRIC_1:4;
then  dist (y,z) >= (dist (x,z)) - (dist (x,y)) by XREAL_1:20;
hence  dist (y,z) >= ((dist_min P) . x) - (dist (x,y)) by A1, XXREAL_0:2; ::_thesis: verum
end;
then  (dist_min P) . y >= ((dist_min P) . x) - (dist (x,y)) by Th14;
hence  (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y) by XREAL_1:20; ::_thesis: verum
end;

theorem Th16: :: HAUSDORF:16
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
let M be non empty MetrSpace; ::_thesis: 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)
let P be Subset of (TopSpaceMetr M); ::_thesis: for Q being non empty Subset of M st P = Q holds
(TopSpaceMetr M) | P = TopSpaceMetr (M | Q)
let Q be non empty Subset of M; ::_thesis: ( P = Q implies (TopSpaceMetr M) | P = TopSpaceMetr (M | Q) )
reconsider N = TopSpaceMetr (M | Q) as SubSpace of TopSpaceMetr M by TOPMETR:13;
A1: the carrier of N = the carrier of (M | Q) by TOPMETR:12;
assume  P = Q ; ::_thesis: (TopSpaceMetr M) | P = TopSpaceMetr (M | Q)
then  [#] N = P by A1, TOPMETR:def_2;
hence  (TopSpaceMetr M) | P = TopSpaceMetr (M | Q) by PRE_TOPC:def_5; ::_thesis: verum
end;

theorem Th17: :: HAUSDORF:17
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 & C is bounded holds
A is bounded
proof
let M be non empty MetrSpace; ::_thesis: for A being Subset of M
for B being non empty Subset of M
for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let A be Subset of M; ::_thesis: for B being non empty Subset of M
for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let B be non empty Subset of M; ::_thesis: for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let C be Subset of (M | B); ::_thesis: ( A = C & C is bounded implies A is bounded )
assume that
A1: A = C and
A2: C is bounded ; ::_thesis: A is bounded
consider r0 being Real such that
A3: 0 < r0 and
A4: for x, y being Point of (M | B) st x in C & y in C holds
dist (x,y) <= r0 by A2, TBSP_1:def_7;
 for x, y being Point of M st x in A & y in A holds
dist (x,y) <= r0
proof
let x, y be Point of M; ::_thesis: ( x in A & y in A implies dist (x,y) <= r0 )
assume A5: ( x in A & y in A ) ; ::_thesis: dist (x,y) <= r0
then reconsider x0 = x, y0 = y as Point of (M | B) by A1;
A6: ( the distance of (M | B) . (x0,y0) = the distance of M . (x,y) & the distance of (M | B) . (x0,y0) = dist (x0,y0) ) by METRIC_1:def_1, TOPMETR:def_1;
 dist (x0,y0) <= r0 by A1, A4, A5;
hence  dist (x,y) <= r0 by A6, METRIC_1:def_1; ::_thesis: verum
end;
hence  A is bounded by A3, TBSP_1:def_7; ::_thesis: verum
end;

theorem :: HAUSDORF:18
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
let M be non empty MetrSpace; ::_thesis: for B being Subset of M
for A being Subset of (TopSpaceMetr M) st A = B & A is compact holds
B is bounded
let B be Subset of M; ::_thesis: for A being Subset of (TopSpaceMetr M) st A = B & A is compact holds
B is bounded
let A be Subset of (TopSpaceMetr M); ::_thesis: ( A = B & A is compact implies B is bounded )
set TA = TopSpaceMetr M;
assume that
A1: A = B and
A2: A is compact ; ::_thesis: B is bounded
 A c= the carrier of ((TopSpaceMetr M) | A) by PRE_TOPC:8;
then reconsider A2 = A as Subset of ((TopSpaceMetr M) | A) ;
percases ( A <> {} or A = {} ) ;
suppose A <> {} ; ::_thesis: B is bounded
then reconsider A1 = A as non empty Subset of M by TOPMETR:12;
 [#] ((TopSpaceMetr M) | A) = A2 by PRE_TOPC:def_5;
then  [#] ((TopSpaceMetr M) | A) is compact by A2, COMPTS_1:2;
then A3: (TopSpaceMetr M) | A is compact by COMPTS_1:1;
 TopSpaceMetr (M | A1) = (TopSpaceMetr M) | A by Th16;
then  M | A1 is totally_bounded by A3, TBSP_1:9;
then  M | A1 is bounded by TBSP_1:19;
then A4: [#] (M | A1) is bounded ;
[#] (M | A1) = the carrier of (M | A1)
.= A1 by TOPMETR:def_2 ;
hence  B is bounded by A1, A4, Th17; ::_thesis: verum
end;
suppose A = {} ; ::_thesis: B is bounded
then  A = {} M ;
hence  B is bounded by A1; ::_thesis: verum
end;
end;
end;

theorem Th19: :: HAUSDORF:19
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
let M be non empty MetrSpace; ::_thesis: 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) )
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for z being Point of M ex w being Point of M st
( w in P & (dist_min P) . z <= dist (w,z) )
let z be Point of M; ::_thesis: ex w being Point of M st
( w in P & (dist_min P) . z <= dist (w,z) )
consider w being set  such that
A1: w in P by XBOOLE_0:def_1;
reconsider w = w as Point of M by A1, TOPMETR:12;
take  w ; ::_thesis: ( w in P & (dist_min P) . z <= dist (w,z) )
thus  w in P by A1; ::_thesis: (dist_min P) . z <= dist (w,z)
thus  (dist_min P) . z <= dist (w,z) by A1, Th13; ::_thesis: verum
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:16;
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:24;
cluster dist_min X ->  continuous ;
coherence
 dist_min X is continuous by WEIERSTR:27;
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
let M be non empty MetrSpace; ::_thesis: 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
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: 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
let x be Point of M; ::_thesis: for X being Subset of REAL st X = (dist x) .: P & P is compact holds
X is bounded_above
let X be Subset of REAL; ::_thesis: ( X = (dist x) .: P & P is compact implies X is bounded_above )
assume  ( X = (dist x) .: P & P is compact ) ; ::_thesis: X is bounded_above
then  ( [#] ((dist x) .: P) is real-bounded & X = [#] ((dist x) .: P) ) by WEIERSTR:9, WEIERSTR:11, WEIERSTR:def_1;
hence  X is bounded_above by XXREAL_2:def_11; ::_thesis: verum
end;

theorem Th20: :: HAUSDORF:20
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
let M be non empty MetrSpace; ::_thesis: 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)
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for x, y being Point of M st y in P & P is compact holds
(dist_max P) . x >= dist (x,y)
let x, y be Point of M; ::_thesis: ( y in P & P is compact implies (dist_max P) . x >= dist (x,y) )
assume that
A1: y in P and
A2: P is compact ; ::_thesis: (dist_max P) . x >= dist (x,y)
consider X being non empty Subset of REAL such that
A3: X = (dist x) .: P and
A4: upper_bound ((dist x) .: P) = upper_bound X by Th11;
A5: (dist_max P) . x = upper_bound X by A4, WEIERSTR:def_5;
 ( dom (dist x) = the carrier of (TopSpaceMetr M) & dist (x,y) = (dist x) . y ) by FUNCT_2:def_1, WEIERSTR:def_4;
then A6: dist (x,y) in X by A1, A3, FUNCT_1:def_6;
 X is bounded_above by A2, A3, Lm1;
hence  (dist_max P) . x >= dist (x,y) by A5, A6, SEQ_4:def_1; ::_thesis: verum
end;

theorem :: HAUSDORF:21
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
let M be non empty MetrSpace; ::_thesis: 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) )
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: 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) )
let z be Point of M; ::_thesis: ( P is compact implies ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) ) )
assume A1: P is compact ; ::_thesis: ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) )
consider w being set  such that
A2: w in P by XBOOLE_0:def_1;
reconsider w = w as Point of M by A2, TOPMETR:12;
take  w ; ::_thesis: ( w in P & (dist_max P) . z >= dist (w,z) )
thus  w in P by A2; ::_thesis: (dist_max P) . z >= dist (w,z)
thus  (dist_max P) . z >= dist (w,z) by A1, A2, Th20; ::_thesis: verum
end;

theorem Th22: :: HAUSDORF:22
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
let M be non empty MetrSpace; ::_thesis: 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)
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: 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)
let z be Point of M; ::_thesis: ( P is compact & Q is compact & z in Q implies (dist_min P) . z <= max_dist_max (P,Q) )
consider w being Point of M such that
A1: w in P and
A2: (dist_min P) . z <= dist (w,z) by Th19;
assume  ( P is compact & Q is compact & z in Q ) ; ::_thesis: (dist_min P) . z <= max_dist_max (P,Q)
then  dist (w,z) <= max_dist_max (P,Q) by A1, WEIERSTR:34;
hence  (dist_min P) . z <= max_dist_max (P,Q) by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem Th23: :: HAUSDORF:23
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
let M be non empty MetrSpace; ::_thesis: 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)
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: 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)
let z be Point of M; ::_thesis: ( P is compact & Q is compact & z in Q implies (dist_max P) . z <= max_dist_max (P,Q) )
assume that
A1: P is compact and
A2: Q is compact ; ::_thesis: ( not z in Q or (dist_max P) . z <= max_dist_max (P,Q) )
reconsider P = P as non empty compact Subset of (TopSpaceMetr M) by A1;
set A = (dist_max P) .: Q;
A3: dom (dist_max P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
assume  z in Q ; ::_thesis: (dist_max P) . z <= max_dist_max (P,Q)
then A4: (dist_max P) . z in (dist_max P) .: Q by A3, FUNCT_1:def_6;
 upper_bound ((dist_max P) .: Q) = max_dist_max (P,Q) by WEIERSTR:def_10;
then consider X being non empty Subset of REAL such that
A5: (dist_max P) .: Q = X and
A6: max_dist_max (P,Q) = upper_bound X by Th11;
 [#] ((dist_max P) .: Q) is real-bounded by A2, WEIERSTR:9, WEIERSTR:11;
then  X is real-bounded by A5, WEIERSTR:def_1;
then  X is bounded_above by XXREAL_2:def_11;
hence  (dist_max P) . z <= max_dist_max (P,Q) by A5, A6, A4, SEQ_4:def_1; ::_thesis: verum
end;

theorem :: HAUSDORF:24
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
let M be non empty MetrSpace; ::_thesis: 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
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: for X being Subset of REAL st X = (dist_max P) .: Q & P is compact & Q is compact holds
X is bounded_above
let X be Subset of REAL; ::_thesis: ( X = (dist_max P) .: Q & P is compact & Q is compact implies X is bounded_above )
assume that
A1: X = (dist_max P) .: Q and
A2: ( P is compact & Q is compact ) ; ::_thesis: X is bounded_above
reconsider Q9 = Q as non empty Subset of M by TOPMETR:12;
 X is bounded_above
proof
take r = max_dist_max (P,Q); :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of X
let p be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not p in X or p <= r )
assume  p in X ; ::_thesis: p <= r
then consider z being set  such that
 z in dom (dist_max P) and
A3: z in Q and
A4: p = (dist_max P) . z by A1, FUNCT_1:def_6;
 z in Q9 by A3;
then reconsider z = z as Point of M ;
 (dist_max P) . z <= r by A2, A3, Th23;
hence  p <= r by A4; ::_thesis: verum
end;
hence  X is bounded_above ; ::_thesis: verum
end;

theorem Th25: :: HAUSDORF:25
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
let M be non empty MetrSpace; ::_thesis: 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
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: for X being Subset of REAL st X = (dist_min P) .: Q & P is compact & Q is compact holds
X is bounded_above
let X be Subset of REAL; ::_thesis: ( X = (dist_min P) .: Q & P is compact & Q is compact implies X is bounded_above )
assume that
A1: X = (dist_min P) .: Q and
A2: ( P is compact & Q is compact ) ; ::_thesis: X is bounded_above
reconsider Q9 = Q as non empty Subset of M by TOPMETR:12;
 X is bounded_above
proof
take r = max_dist_max (P,Q); :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of X
let p be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not p in X or p <= r )
assume  p in X ; ::_thesis: p <= r
then consider z being set  such that
 z in dom (dist_min P) and
A3: z in Q and
A4: p = (dist_min P) . z by A1, FUNCT_1:def_6;
 z in Q9 by A3;
then reconsider z = z as Point of M ;
 (dist_min P) . z <= r by A2, A3, Th22;
hence  p <= r by A4; ::_thesis: verum
end;
hence  X is bounded_above ; ::_thesis: verum
end;

theorem :: HAUSDORF:26
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
let M be non empty MetrSpace; ::_thesis: 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
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: for z being Point of M st P is compact holds
(dist_min P) . z <= (dist_max P) . z
let z be Point of M; ::_thesis: ( P is compact implies (dist_min P) . z <= (dist_max P) . z )
consider w being Point of M such that
A1: w in P and
A2: (dist_min P) . z <= dist (w,z) by Th19;
assume  P is compact ; ::_thesis: (dist_min P) . z <= (dist_max P) . z
then  (dist_max P) . z >= dist (z,w) by A1, Th20;
hence  (dist_min P) . z <= (dist_max P) . z by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem Th27: :: HAUSDORF:27
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0}
proof
let M be non empty MetrSpace; ::_thesis: for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0}
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: (dist_min P) .: P = {0}
consider x being set  such that
A1: x in P by XBOOLE_0:def_1;
thus  (dist_min P) .: P c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= (dist_min P) .: P
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (dist_min P) .: P or y in {0} )
assume  y in (dist_min P) .: P ; ::_thesis: y in {0}
then  ex x being set st
( x in dom (dist_min P) & x in P & y = (dist_min P) . x ) by FUNCT_1:def_6;
then  y = 0 by Th5;
hence  y in {0} by TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {0} or y in (dist_min P) .: P )
A2: dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
assume  y in {0} ; ::_thesis: y in (dist_min P) .: P
then  y = 0 by TARSKI:def_1;
then  y = (dist_min P) . x by A1, Th5;
hence  y in (dist_min P) .: P by A1, A2, FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th28: :: HAUSDORF:28
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
let M be non empty MetrSpace; ::_thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
max_dist_min (P,Q) >= 0
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact implies max_dist_min (P,Q) >= 0 )
assume  ( P is compact & Q is compact ) ; ::_thesis: max_dist_min (P,Q) >= 0
then  ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) by WEIERSTR:32;
hence  max_dist_min (P,Q) >= 0 by METRIC_1:5; ::_thesis: verum
end;

theorem Th29: :: HAUSDORF:29
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds max_dist_min (P,P) = 0
proof
let M be non empty MetrSpace; ::_thesis: for P being non empty Subset of (TopSpaceMetr M) holds max_dist_min (P,P) = 0
let P be non empty Subset of (TopSpaceMetr M); ::_thesis: max_dist_min (P,P) = 0
A1: [#] ((dist_min P) .: P) = (dist_min P) .: P by WEIERSTR:def_1
.= {0} by Th27 ;
max_dist_min (P,P) = upper_bound ((dist_min P) .: P) by WEIERSTR:def_8
.= upper_bound {0} by A1, WEIERSTR:def_2 ;
hence  max_dist_min (P,P) = 0 by SEQ_4:9; ::_thesis: verum
end;

theorem :: HAUSDORF:30
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
let M be non empty MetrSpace; ::_thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
min_dist_max (P,Q) >= 0
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact implies min_dist_max (P,Q) >= 0 )
assume  ( P is compact & Q is compact ) ; ::_thesis: min_dist_max (P,Q) >= 0
then  ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) by WEIERSTR:31;
hence  min_dist_max (P,Q) >= 0 by METRIC_1:5; ::_thesis: verum
end;

theorem Th31: :: HAUSDORF:31
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
let M be non empty MetrSpace; ::_thesis: 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)
let Q, R be non empty Subset of (TopSpaceMetr M); ::_thesis: 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)
let y be Point of M; ::_thesis: ( Q is compact & R is compact & y in Q implies (dist_min R) . y <= max_dist_min (R,Q) )
assume that
A1: ( Q is compact & R is compact ) and
A2: y in Q ; ::_thesis: (dist_min R) . y <= max_dist_min (R,Q)
set A = (dist_min R) .: Q;
consider X being non empty Subset of REAL such that
A3: (dist_min R) .: Q = X and
A4: upper_bound ((dist_min R) .: Q) = upper_bound X by Th11;
 dom (dist_min R) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then A5: (dist_min R) . y in X by A2, A3, FUNCT_1:def_6;
 ( max_dist_min (R,Q) = upper_bound ((dist_min R) .: Q) & X is bounded_above ) by A1, A3, Th25, WEIERSTR:def_8;
hence  (dist_min R) . y <= max_dist_min (R,Q) by A4, A5, SEQ_4:def_1; ::_thesis: verum
end;

begin

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 Th32: :: HAUSDORF:32
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
let M be non empty MetrSpace; ::_thesis: 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)
let Q, R be non empty Subset of (TopSpaceMetr M); ::_thesis: for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= HausDist (Q,R)
let y be Point of M; ::_thesis: ( Q is compact & R is compact & y in Q implies (dist_min R) . y <= HausDist (Q,R) )
assume  ( Q is compact & R is compact & y in Q ) ; ::_thesis: (dist_min R) . y <= HausDist (Q,R)
then  ( max_dist_min (R,Q) <= max ((max_dist_min (R,Q)),(max_dist_min (Q,R))) & (dist_min R) . y <= max_dist_min (R,Q) ) by Th31, XXREAL_0:25;
hence  (dist_min R) . y <= HausDist (Q,R) by XXREAL_0:2; ::_thesis: verum
end;

theorem Th33: :: HAUSDORF:33
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
let M be non empty MetrSpace; ::_thesis: 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))
let P, Q, R be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact & R is compact implies max_dist_min (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume that
A1: P is compact and
A2: Q is compact and
A3: R is compact ; ::_thesis: max_dist_min (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R))
reconsider DPR = (dist_min P) .: R as non empty Subset of REAL by TOPMETR:17;
A4: for w being real number st w in DPR holds
w <= (HausDist (P,Q)) + (HausDist (Q,R))
proof
let w be real number ; ::_thesis: ( w in DPR implies w <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume  w in DPR ; ::_thesis: w <= (HausDist (P,Q)) + (HausDist (Q,R))
then consider y being set  such that
 y in dom (dist_min P) and
A5: y in R and
A6: w = (dist_min P) . y by FUNCT_1:def_6;
reconsider y = y as Point of M by A5, TOPMETR:12;
 for z being Point of M st z in Q holds
dist (y,z) >= ((dist_min P) . y) - (HausDist (Q,P))
proof
let z be Point of M; ::_thesis: ( z in Q implies dist (y,z) >= ((dist_min P) . y) - (HausDist (Q,P)) )
assume  z in Q ; ::_thesis: dist (y,z) >= ((dist_min P) . y) - (HausDist (Q,P))
then  (dist_min P) . z <= HausDist (Q,P) by A1, A2, Th32;
then A7: (dist (y,z)) + ((dist_min P) . z) <= (dist (y,z)) + (HausDist (Q,P)) by XREAL_1:6;
 (dist_min P) . y <= (dist (y,z)) + ((dist_min P) . z) by Th15;
then  (dist_min P) . y <= (dist (y,z)) + (HausDist (Q,P)) by A7, XXREAL_0:2;
hence  dist (y,z) >= ((dist_min P) . y) - (HausDist (Q,P)) by XREAL_1:20; ::_thesis: verum
end;
then  ((dist_min P) . y) - (HausDist (Q,P)) <= (dist_min Q) . y by Th14;
then A8: (dist_min P) . y <= (HausDist (Q,P)) + ((dist_min Q) . y) by XREAL_1:20;
 (dist_min Q) . y <= HausDist (R,Q) by A2, A3, A5, Th32;
then  (HausDist (Q,P)) + ((dist_min Q) . y) <= (HausDist (Q,P)) + (HausDist (Q,R)) by XREAL_1:6;
hence  w <= (HausDist (P,Q)) + (HausDist (Q,R)) by A6, A8, XXREAL_0:2; ::_thesis: verum
end;
upper_bound DPR = upper_bound ([#] ((dist_min P) .: R)) by WEIERSTR:def_1
.= upper_bound ((dist_min P) .: R) by WEIERSTR:def_2
.= max_dist_min (P,R) by WEIERSTR:def_8 ;
hence  max_dist_min (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) by A4, SEQ_4:45; ::_thesis: verum
end;

theorem :: HAUSDORF:34
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
let M be non empty MetrSpace; ::_thesis: 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))
let P, Q, R be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact & R is compact implies max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume that
A1: P is compact and
A2: Q is compact and
A3: R is compact ; ::_thesis: max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R))
reconsider DPR = (dist_min R) .: P as non empty Subset of REAL by TOPMETR:17;
A4: for w being real number st w in DPR holds
w <= (HausDist (P,Q)) + (HausDist (Q,R))
proof
let w be real number ; ::_thesis: ( w in DPR implies w <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume  w in DPR ; ::_thesis: w <= (HausDist (P,Q)) + (HausDist (Q,R))
then consider y being set  such that
 y in dom (dist_min R) and
A5: y in P and
A6: w = (dist_min R) . y by FUNCT_1:def_6;
reconsider y = y as Point of M by A5, TOPMETR:12;
 for z being Point of M st z in Q holds
dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R))
proof
let z be Point of M; ::_thesis: ( z in Q implies dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R)) )
assume  z in Q ; ::_thesis: dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R))
then  (dist_min R) . z <= HausDist (Q,R) by A2, A3, Th32;
then A7: (dist (y,z)) + ((dist_min R) . z) <= (dist (y,z)) + (HausDist (Q,R)) by XREAL_1:6;
 (dist_min R) . y <= (dist (y,z)) + ((dist_min R) . z) by Th15;
then  (dist_min R) . y <= (dist (y,z)) + (HausDist (Q,R)) by A7, XXREAL_0:2;
hence  dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R)) by XREAL_1:20; ::_thesis: verum
end;
then A8: ((dist_min R) . y) - (HausDist (Q,R)) <= (dist_min Q) . y by Th14;
 (dist_min Q) . y <= HausDist (P,Q) by A1, A2, A5, Th32;
then  ((dist_min R) . y) - (HausDist (Q,R)) <= HausDist (P,Q) by A8, XXREAL_0:2;
hence  w <= (HausDist (P,Q)) + (HausDist (Q,R)) by A6, XREAL_1:20; ::_thesis: verum
end;
upper_bound DPR = upper_bound ([#] ((dist_min R) .: P)) by WEIERSTR:def_1
.= upper_bound ((dist_min R) .: P) by WEIERSTR:def_2
.= max_dist_min (R,P) by WEIERSTR:def_8 ;
hence  max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) by A4, SEQ_4:45; ::_thesis: verum
end;

theorem Th35: :: HAUSDORF:35
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
let M be non empty MetrSpace; ::_thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
HausDist (P,Q) >= 0
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact implies HausDist (P,Q) >= 0 )
assume A1: ( P is compact & Q is compact ) ; ::_thesis: HausDist (P,Q) >= 0
percases ( HausDist (P,Q) = max_dist_min (P,Q) or HausDist (P,Q) = max_dist_min (Q,P) ) by XXREAL_0:16;
suppose HausDist (P,Q) = max_dist_min (P,Q) ; ::_thesis: HausDist (P,Q) >= 0
hence  HausDist (P,Q) >= 0 by A1, Th28; ::_thesis: verum
end;
suppose HausDist (P,Q) = max_dist_min (Q,P) ; ::_thesis: HausDist (P,Q) >= 0
hence  HausDist (P,Q) >= 0 by A1, Th28; ::_thesis: verum
end;
end;
end;

theorem :: HAUSDORF:36
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M) holds HausDist (P,P) = 0 by Th29;

theorem Th37: :: HAUSDORF:37
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
let M be non empty MetrSpace; ::_thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & HausDist (P,Q) = 0 holds
P = Q
let P, Q be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact & HausDist (P,Q) = 0 implies P = Q )
assume that
A1: P is compact and
A2: Q is compact ; ::_thesis: ( not HausDist (P,Q) = 0 or P = Q )
A3: Q is closed by A2, COMPTS_1:7;
assume A4: HausDist (P,Q) = 0 ; ::_thesis: P = Q
then  max_dist_min (Q,P) = 0 by A1, A2, Th1, Th28;
then  upper_bound ((dist_min Q) .: P) = 0 by WEIERSTR:def_8;
then consider Y being non empty Subset of REAL such that
A5: (dist_min Q) .: P = Y and
A6: 0 = upper_bound Y by Th11;
A7: Y is bounded_above by A1, A2, A5, Th25;
thus  P c= Q :: according to XBOOLE_0:def_10 ::_thesis: Q c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in Q )
assume A8: x in P ; ::_thesis: x in Q
then reconsider x9 = x as Point of M by TOPMETR:12;
 dom (dist_min Q) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then  (dist_min Q) . x in Y by A5, A8, FUNCT_1:def_6;
then A9: (dist_min Q) . x <= 0 by A6, A7, SEQ_4:def_1;
 (dist_min Q) . x >= 0 by A8, JORDAN1K:9;
then  (dist_min Q) . x = 0 by A9, XXREAL_0:1;
then  x9 in Q by A3, Th9;
hence  x in Q ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in P )
assume A10: x in Q ; ::_thesis: x in P
then reconsider x9 = x as Point of M by TOPMETR:12;
A11: P is closed by A1, COMPTS_1:7;
 max_dist_min (P,Q) = 0 by A1, A2, A4, Th1, Th28;
then  upper_bound ((dist_min P) .: Q) = 0 by WEIERSTR:def_8;
then consider X being non empty Subset of REAL such that
A12: (dist_min P) .: Q = X and
A13: 0 = upper_bound X by Th11;
 dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1;
then A14: (dist_min P) . x in X by A12, A10, FUNCT_1:def_6;
 X is bounded_above by A1, A2, A12, Th25;
then A15: (dist_min P) . x <= 0 by A13, A14, SEQ_4:def_1;
 (dist_min P) . x >= 0 by A10, JORDAN1K:9;
then  (dist_min P) . x = 0 by A15, XXREAL_0:1;
then  x9 in P by A11, Th9;
hence  x in P ; ::_thesis: verum
end;

theorem Th38: :: HAUSDORF:38
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
let M be non empty MetrSpace; ::_thesis: 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))
let P, Q, R be non empty Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact & R is compact implies HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume  ( P is compact & Q is compact & R is compact ) ; ::_thesis: HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R))
then  ( max_dist_min (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) & max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) ) by Th33;
hence  HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) by XXREAL_0:28; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let P, Q be Subset of (TOP-REAL n);
func max_dist_min (P,Q) ->  Real means :: HAUSDORF:def 2
 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) )
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid n)) ;
take  max_dist_min (P9,Q9) ; ::_thesis: ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) )
take  P9 ; ::_thesis: ex Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) )
take  Q9 ; ::_thesis: ( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) )
thus  ( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) ) ; ::_thesis: verum
end;
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: :: HAUSDORF:def 3
 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) )
proof
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid n)) ;
take  HausDist (P9,Q9) ; ::_thesis: ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & HausDist (P9,Q9) = HausDist (P9,Q9) )
take  P9 ; ::_thesis: ex Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & HausDist (P9,Q9) = HausDist (P9,Q9) )
take  Q9 ; ::_thesis: ( P = P9 & Q = Q9 & HausDist (P9,Q9) = HausDist (P9,Q9) )
thus  ( P = P9 & Q = Q9 & HausDist (P9,Q9) = HausDist (P9,Q9) ) ; ::_thesis: verum
end;
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 :: HAUSDORF:39
for n being Element of 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
let n be Element of NAT ; ::_thesis: for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact holds
HausDist (P,Q) >= 0
let P, Q be non empty Subset of (TOP-REAL n); ::_thesis: ( P is compact & Q is compact implies HausDist (P,Q) >= 0 )
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider P1 = P, Q1 = Q as non empty Subset of (TopSpaceMetr (Euclid n)) ;
assume  ( P is compact & Q is compact ) ; ::_thesis: HausDist (P,Q) >= 0
then  ( P1 is compact & Q1 is compact ) by A1, COMPTS_1:23;
then  HausDist (P1,Q1) >= 0 by Th35;
hence  HausDist (P,Q) >= 0 by Def3; ::_thesis: verum
end;

theorem :: HAUSDORF:40
for n being Element of NAT
for P being non empty Subset of (TOP-REAL n) holds HausDist (P,P) = 0
proof
let n be Element of NAT ; ::_thesis: for P being non empty Subset of (TOP-REAL n) holds HausDist (P,P) = 0
let P be non empty Subset of (TOP-REAL n); ::_thesis: HausDist (P,P) = 0
 TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider P1 = P as non empty Subset of (TopSpaceMetr (Euclid n)) ;
 HausDist (P1,P1) = 0 by Th29;
hence  HausDist (P,P) = 0 by Def3; ::_thesis: verum
end;

theorem :: HAUSDORF:41
for n being Element of 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
let n be Element of NAT ; ::_thesis: 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
let P, Q be non empty Subset of (TOP-REAL n); ::_thesis: ( P is compact & Q is compact & HausDist (P,Q) = 0 implies P = Q )
assume that
A1: ( P is compact & Q is compact ) and
A2: HausDist (P,Q) = 0 ; ::_thesis: P = Q
A3: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider P1 = P, Q1 = Q as non empty Subset of (TopSpaceMetr (Euclid n)) ;
A4: HausDist (P1,Q1) = 0 by A2, Def3;
 ( P1 is compact & Q1 is compact ) by A1, A3, COMPTS_1:23;
hence  P = Q by A4, Th37; ::_thesis: verum
end;

theorem :: HAUSDORF:42
for n being Element of 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
let n be Element of NAT ; ::_thesis: 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))
let P, Q, R be non empty Subset of (TOP-REAL n); ::_thesis: ( P is compact & Q is compact & R is compact implies HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume that
A1: ( P is compact & Q is compact ) and
A2: R is compact ; ::_thesis: HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R))
A3: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider P1 = P, Q1 = Q, R1 = R as non empty Subset of (TopSpaceMetr (Euclid n)) ;
A4: R1 is compact by A2, A3, COMPTS_1:23;
A5: HausDist (Q1,R1) = HausDist (Q,R) by Def3;
A6: ( HausDist (P1,R1) = HausDist (P,R) & HausDist (P1,Q1) = HausDist (P,Q) ) by Def3;
 ( P1 is compact & Q1 is compact ) by A1, A3, COMPTS_1:23;
hence  HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) by A4, A6, A5, Th38; ::_thesis: verum
end;