:: by Adam Grabowski

::

:: Received January 27, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

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

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

for M being non empty MetrSpace

for P being Subset of (TopSpaceMetr M)

for x being Point of M

for y being Real st y in (dist x) .: P holds

y >= 0

for P being Subset of (TopSpaceMetr M)

for x being Point of M

for y being Real st y in (dist x) .: P holds

y >= 0

proof 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

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

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 st r > 0 holds

ex q being Point of M st

( q in A & dist (p,q) < r ) )

for p being Point of M

for A being Subset of (TopSpaceMetr M) holds

( p in Cl A iff for r being Real st r > 0 holds

ex q being Point of M st

( q in A & dist (p,q) < r ) )

proof 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 st r > 0 holds

ex p being Point of M st

( p in P & dist (x,p) < r ) )

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 st r > 0 holds

ex p being Point of M st

( p in P & dist (x,p) < r ) )

proof 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 )

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 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 )

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 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 )

( A = X & lower_bound A = lower_bound X )

proof 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 )

( A = X & upper_bound A = upper_bound X )

proof 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

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 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)

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 Th14: :: HAUSDORF:14

for M being non empty MetrSpace

for P being non empty Subset of (TopSpaceMetr M)

for r being Real

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

for P being non empty Subset of (TopSpaceMetr M)

for r being Real

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 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)

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 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)

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 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

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 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

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 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) )

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

registration

let M be non empty MetrSpace;

let X be non empty compact Subset of (TopSpaceMetr M);

coherence

dist_max X is continuous by WEIERSTR:24;

coherence

dist_min X is continuous by WEIERSTR:27;

end;
let X be non empty compact Subset of (TopSpaceMetr M);

coherence

dist_max X is continuous by WEIERSTR:24;

coherence

dist_min X is continuous by WEIERSTR:27;

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 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)

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: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) )

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 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)

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 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)

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: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

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 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

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: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

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 Th27: :: HAUSDORF:27

for M being non empty MetrSpace

for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0}

for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0}

proof 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

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 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

for P being non empty Subset of (TopSpaceMetr M) holds max_dist_min (P,P) = 0

proof 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

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 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)

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);

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is Real ;

commutativity

for b_{1} being Real

for P, Q being Subset of (TopSpaceMetr M) st b_{1} = max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) holds

b_{1} = max ((max_dist_min (Q,P)),(max_dist_min (P,Q)))
;

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

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is Real ;

commutativity

for b

for P, Q being Subset of (TopSpaceMetr M) st b

b

:: 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)));

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)

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 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))

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 :: 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))

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 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

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 :: HAUSDORF:36

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

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 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))

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 Element of NAT ;

let P, Q be Subset of (TOP-REAL n);

ex b_{1} being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{1} = max_dist_min (P9,Q9) )

for b_{1}, b_{2} being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{1} = max_dist_min (P9,Q9) ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{2} = max_dist_min (P9,Q9) ) holds

b_{1} = b_{2}
;

end;
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 P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & it = max_dist_min (P9,Q9) );

ex b

( P = P9 & Q = Q9 & b

proof end;

uniqueness for b

( P = P9 & Q = Q9 & b

( P = P9 & Q = Q9 & b

b

:: deftheorem defines max_dist_min HAUSDORF:def 2 :

for n being Element of NAT

for P, Q being Subset of (TOP-REAL n)

for b_{4} being Real holds

( b_{4} = max_dist_min (P,Q) iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{4} = max_dist_min (P9,Q9) ) );

for n being Element of NAT

for P, Q being Subset of (TOP-REAL n)

for b

( b

( P = P9 & Q = Q9 & b

definition

let n be Element of NAT ;

let P, Q be Subset of (TOP-REAL n);

ex b_{1} being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{1} = HausDist (P9,Q9) )

for b_{1}, b_{2} being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{1} = HausDist (P9,Q9) ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{2} = HausDist (P9,Q9) ) holds

b_{1} = b_{2}
;

commutativity

for b_{1} 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 & b_{1} = HausDist (P9,Q9) ) holds

ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( Q = P9 & P = Q9 & b_{1} = HausDist (P9,Q9) )
;

end;
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 P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & it = HausDist (P9,Q9) );

ex b

( P = P9 & Q = Q9 & b

proof end;

uniqueness for b

( P = P9 & Q = Q9 & b

( P = P9 & Q = Q9 & b

b

commutativity

for b

for P, Q being Subset of (TOP-REAL n) st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b

ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( Q = P9 & P = Q9 & b

:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :

for n being Element of NAT

for P, Q being Subset of (TOP-REAL n)

for b_{4} being Real holds

( b_{4} = HausDist (P,Q) iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st

( P = P9 & Q = Q9 & b_{4} = HausDist (P9,Q9) ) );

for n being Element of NAT

for P, Q being Subset of (TOP-REAL n)

for b

( b

( P = P9 & Q = Q9 & b

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

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: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

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: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))

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;