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