hausdorf.miz



    begin

    registration

      let M be non empty MetrSpace;

      cluster ( TopSpaceMetr M) -> T_2;

      coherence by PCOMPS_1: 34;

    end

    theorem :: HAUSDORF:1

    

     Th1: for x,y be Real st x >= 0 & ( max (x,y)) = 0 holds x = 0

    proof

      let x,y be Real;

      assume that

       A1: x >= 0 and

       A2: ( max (x,y)) = 0 ;

      per cases by XXREAL_0: 16;

        suppose ( max (x,y)) = x;

        hence thesis by A2;

      end;

        suppose

         A3: ( max (x,y)) = y;

        then x <= y by XXREAL_0: 25;

        hence thesis by A1, A2, A3, XXREAL_0: 1;

      end;

    end;

    theorem :: HAUSDORF:2

    

     Th2: for M be non empty MetrSpace, x be Point of M holds (( dist x) . x) = 0

    proof

      let M be non empty MetrSpace, x be Point of M;

      (( dist x) . x) = ( dist (x,x)) by WEIERSTR:def 4

      .= 0 by METRIC_1: 1;

      hence thesis;

    end;

    theorem :: HAUSDORF:3

    

     Th3: for M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), x be Point of M st x in P holds 0 in (( dist x) .: P)

    proof

      let M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), x be Point of M;

      

       A1: ( dom ( dist x)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

      assume x in P;

      then (( dist x) . x) in (( dist x) .: P) by A1, FUNCT_1:def 6;

      hence thesis by Th2;

    end;

    theorem :: HAUSDORF:4

    

     Th4: for M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), x be Point of M, y be Real st y in (( dist x) .: P) holds y >= 0

    proof

      let M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), x be Point of M, y be Real;

      assume y in (( dist x) .: P);

      then

      consider z be object 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 thesis by METRIC_1: 5;

    end;

    theorem :: HAUSDORF:5

    

     Th5: for M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), x be set st x in P holds (( dist_min P) . x) = 0

    proof

      let M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), x be set;

      assume

       A1: x in P;

      then

      reconsider x as Point of M by TOPMETR: 12;

      set X = (( dist x) .: P);

      reconsider X 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 be Real st p in X holds p >= 0 by Th4;

      for q be Real st for p be Real st p in X holds p >= q holds 0 >= q by A1, Th3;

      hence thesis by A2, A3, SEQ_4: 44;

    end;

    theorem :: HAUSDORF:6

    

     Th6: for M be non empty MetrSpace, p be Point of M, A be Subset of ( TopSpaceMetr M) holds p in ( Cl A) iff for r be Real st r > 0 holds ex q be Point of M st q in A & ( dist (p,q)) < r

    proof

      let M be non empty MetrSpace, p be Point of M, A be Subset of ( TopSpaceMetr M);

      hereby

        assume

         A1: p in ( Cl A);

        let r be Real;

        assume r > 0 ;

        then ( Ball (p,r)) meets A by A1, GOBOARD6: 92;

        then

        consider x be object 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;

        thus q in A by A3;

        thus ( dist (p,q)) < r by A2, METRIC_1: 11;

      end;

      assume

       A4: for r be Real st r > 0 holds ex q be Point of M st q in A & ( dist (p,q)) < r;

      for r be Real st r > 0 holds ( Ball (p,r)) meets A

      proof

        let r be Real;

        assume r > 0 ;

        then

        consider q be 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 thesis by A5, XBOOLE_0: 3;

      end;

      hence thesis by GOBOARD6: 92;

    end;

    theorem :: HAUSDORF:7

    

     Th7: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M holds (( dist_min P) . x) = 0 iff for r be Real st r > 0 holds ex p be Point of M st p in P & ( dist (x,p)) < r

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M;

      reconsider X = (( dist x) .: P) as non empty Subset of REAL by TOPMETR: 17;

      hereby

        assume

         A1: (( dist_min P) . x) = 0 ;

        let r be Real;

        assume

         A2: r > 0 ;

        assume

         A3: for p be Point of M st p in P holds ( dist (x,p)) >= r;

        for p be Real st p in X holds p >= r

        proof

          let p be Real;

          assume p in X;

          then

          consider y be object 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 thesis by A6, WEIERSTR:def 4;

        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;

      end;

      

       A8: for p be Real st p in X holds p >= 0

      proof

        let p be Real;

        assume p in X;

        then

        consider y be object 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 thesis by A10, WEIERSTR:def 4;

      end;

      assume

       A11: for r be Real st r > 0 holds ex p be Point of M st p in P & ( dist (x,p)) < r;

      

       A12: for q be Real st for p be Real st p in X holds p >= q holds 0 >= q

      proof

        let q be Real;

        assume

         A13: for z be Real st z in X holds z >= q;

        assume 0 < q;

        then

        consider p be 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: z in X by A14, FUNCT_1:def 6;

        (( dist x) . p) < q by A15, WEIERSTR:def 4;

        hence thesis by A13, A16;

      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 thesis by WEIERSTR:def 6;

    end;

    theorem :: HAUSDORF:8

    

     Th8: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M holds x in ( Cl P) iff (( dist_min P) . x) = 0

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M;

      hereby

        assume x in ( Cl P);

        then for a be Real st a > 0 holds ex p be Point of M st p in P & ( dist (x,p)) < a by Th6;

        hence (( dist_min P) . x) = 0 by Th7;

      end;

      assume (( dist_min P) . x) = 0 ;

      then for a be Real st a > 0 holds ex p be Point of M st p in P & ( dist (x,p)) < a by Th7;

      hence thesis by Th6;

    end;

    theorem :: HAUSDORF:9

    

     Th9: for M be non empty MetrSpace, P be non empty closed Subset of ( TopSpaceMetr M), x be Point of M holds x in P iff (( dist_min P) . x) = 0

    proof

      let M be non empty MetrSpace, P be non empty closed Subset of ( TopSpaceMetr M), x be Point of M;

      P = ( Cl P) by PRE_TOPC: 22;

      hence thesis by Th8;

    end;

    theorem :: HAUSDORF:10

    

     Th10: for A be non empty Subset of R^1 holds ex X be non empty Subset of REAL st A = X & ( lower_bound A) = ( lower_bound X)

    proof

      let A be non empty Subset of R^1 ;

      reconsider X = A as non empty Subset of REAL by TOPMETR: 17;

      take X;

      ( lower_bound A) = ( lower_bound ( [#] A)) by WEIERSTR:def 3

      .= ( lower_bound X) by WEIERSTR:def 1;

      hence thesis;

    end;

    theorem :: HAUSDORF:11

    

     Th11: for A be non empty Subset of R^1 holds ex X be non empty Subset of REAL st A = X & ( upper_bound A) = ( upper_bound X)

    proof

      let A be non empty Subset of R^1 ;

      reconsider X = A as non empty Subset of REAL by TOPMETR: 17;

      take X;

      ( upper_bound A) = ( upper_bound ( [#] A)) by WEIERSTR:def 2

      .= ( upper_bound X) by WEIERSTR:def 1;

      hence thesis;

    end;

    theorem :: HAUSDORF:12

    

     Th12: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M, X be Subset of REAL st X = (( dist x) .: P) holds X is bounded_below

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M, X be Subset of REAL ;

      assume

       A1: X = (( dist x) .: P);

      take 0 ;

      let y be ExtReal;

      thus y in X implies 0 <= y by A1, Th4;

    end;

    theorem :: HAUSDORF:13

    

     Th13: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x,y be Point of M st y in P holds (( dist_min P) . x) <= ( dist (x,y))

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x,y be Point of M;

      

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

      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 thesis by A4, SEQ_4:def 2;

    end;

    theorem :: HAUSDORF:14

    

     Th14: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), r be Real, x be Point of M holds (for y be Point of M st y in P holds ( dist (x,y)) >= r) implies (( dist_min P) . x) >= r

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), r be Real, x be Point of M;

      consider X be 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 be Point of M st y in P holds ( dist (x,y)) >= r;

      for p be Real st p in X holds p >= r

      proof

        let p be Real;

        assume p in X;

        then

        consider y be object 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 as Point of M by A4, TOPMETR: 12;

        p = ( dist (x,y)) by A6, WEIERSTR:def 4;

        hence thesis by A3, A5;

      end;

      then ( lower_bound X) >= r by SEQ_4: 43;

      hence thesis by A2, WEIERSTR:def 6;

    end;

    theorem :: HAUSDORF:15

    

     Th15: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x,y be Point of M holds (( dist_min P) . x) <= (( dist (x,y)) + (( dist_min P) . y))

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x,y be Point of M;

      now

        let z be Point of M;

        assume z in P;

        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;

      end;

      then (( dist_min P) . y) >= ((( dist_min P) . x) - ( dist (x,y))) by Th14;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: HAUSDORF:16

    

     Th16: for M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), Q be non empty Subset of M holds P = Q implies (( TopSpaceMetr M) | P) = ( TopSpaceMetr (M | Q))

    proof

      let M be non empty MetrSpace, P be Subset of ( TopSpaceMetr M), Q be non empty Subset of M;

      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;

      then ( [#] N) = P by A1, TOPMETR:def 2;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: HAUSDORF:17

    

     Th17: for M be non empty MetrSpace, A be Subset of M, B be non empty Subset of M, C be Subset of (M | B) st A = C & C is bounded holds A is bounded

    proof

      let M be non empty MetrSpace, A be Subset of M, B be non empty Subset of M, C be Subset of (M | B);

      assume that

       A1: A = C and

       A2: C is bounded;

      consider r0 be Real such that

       A3: 0 < r0 and

       A4: for x,y be 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 be Point of M st x in A & y in A holds ( dist (x,y)) <= r0

      proof

        let x,y be Point of M;

        assume

         A5: x in A & y in A;

        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 thesis by A6, METRIC_1:def 1;

      end;

      hence thesis by A3, TBSP_1:def 7;

    end;

    theorem :: HAUSDORF:18

    for M be non empty MetrSpace, B be Subset of M, A be Subset of ( TopSpaceMetr M) st A = B & A is compact holds B is bounded

    proof

      let M be non empty MetrSpace, B be Subset of M, A be Subset of ( TopSpaceMetr M);

      set TA = ( TopSpaceMetr M);

      assume that

       A1: A = B and

       A2: A is compact;

      A c= the carrier of (TA | A) by PRE_TOPC: 8;

      then

      reconsider A2 = A as Subset of (TA | A);

      per cases ;

        suppose A <> {} ;

        then

        reconsider A1 = A as non empty Subset of M by TOPMETR: 12;

        ( [#] (TA | A)) = A2 by PRE_TOPC:def 5;

        then ( [#] (TA | A)) is compact by A2, COMPTS_1: 2;

        then

         A3: (TA | A) is compact by COMPTS_1: 1;

        ( TopSpaceMetr (M | A1)) = (TA | 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 thesis by A1, A4, Th17;

      end;

        suppose A = {} ;

        then A = ( {} M);

        hence thesis by A1;

      end;

    end;

    theorem :: HAUSDORF:19

    

     Th19: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), z be Point of M holds ex w be Point of M st w in P & (( dist_min P) . z) <= ( dist (w,z))

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), z be Point of M;

      consider w be object such that

       A1: w in P by XBOOLE_0:def 1;

      reconsider w as Point of M by A1, TOPMETR: 12;

      take w;

      thus w in P by A1;

      thus thesis by A1, Th13;

    end;

    registration

      let M be non empty MetrSpace, x be Point of M;

      cluster ( dist x) -> continuous;

      coherence by WEIERSTR: 16;

    end

    registration

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

      cluster ( dist_max X) -> continuous;

      coherence by WEIERSTR: 24;

      cluster ( dist_min X) -> continuous;

      coherence by WEIERSTR: 27;

    end

    

     Lm1: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M, X be Subset of REAL st X = (( dist x) .: P) & P is compact holds X is bounded_above

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x be Point of M, X be Subset of REAL ;

      assume X = (( dist x) .: P) & P is compact;

      then ( [#] (( dist x) .: P)) is real-bounded & X = ( [#] (( dist x) .: P)) by WEIERSTR: 9, WEIERSTR: 11, WEIERSTR:def 1;

      hence thesis;

    end;

    theorem :: HAUSDORF:20

    

     Th20: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), x,y be 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, P be non empty Subset of ( TopSpaceMetr M), x,y be Point of M;

      assume that

       A1: y in P and

       A2: P is compact;

      consider X be 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 thesis by A5, A6, SEQ_4:def 1;

    end;

    theorem :: HAUSDORF:21

    for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), z be Point of M st P is compact holds ex w be Point of M st w in P & (( dist_max P) . z) >= ( dist (w,z))

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), z be Point of M;

      assume

       A1: P is compact;

      consider w be object such that

       A2: w in P by XBOOLE_0:def 1;

      reconsider w as Point of M by A2, TOPMETR: 12;

      take w;

      thus w in P by A2;

      thus thesis by A1, A2, Th20;

    end;

    theorem :: HAUSDORF:22

    

     Th22: for M be non empty MetrSpace, P,Q be non empty Subset of ( TopSpaceMetr M), z be 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, P,Q be non empty Subset of ( TopSpaceMetr M), z be Point of M;

      consider w be 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;

      then ( dist (w,z)) <= ( max_dist_max (P,Q)) by A1, WEIERSTR: 34;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: HAUSDORF:23

    

     Th23: for M be non empty MetrSpace, P,Q be non empty Subset of ( TopSpaceMetr M), z be 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, P,Q be non empty Subset of ( TopSpaceMetr M), z be Point of M;

      assume that

       A1: P is compact and

       A2: Q is compact;

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

      then

       A4: (( dist_max P) . z) in A by A3, FUNCT_1:def 6;

      ( upper_bound (( dist_max P) .: Q)) = ( max_dist_max (P,Q)) by WEIERSTR:def 10;

      then

      consider X be non empty Subset of REAL such that

       A5: A = X and

       A6: ( max_dist_max (P,Q)) = ( upper_bound X) by Th11;

      ( [#] A) is real-bounded by A2, WEIERSTR: 9, WEIERSTR: 11;

      then X is real-bounded by A5, WEIERSTR:def 1;

      then X is bounded_above;

      hence thesis by A5, A6, A4, SEQ_4:def 1;

    end;

    theorem :: HAUSDORF:24

    for M be non empty MetrSpace, P,Q be non empty Subset of ( TopSpaceMetr M), X be 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, P,Q be non empty Subset of ( TopSpaceMetr M), X be Subset of REAL ;

      assume that

       A1: X = (( dist_max P) .: Q) and

       A2: P is compact & Q is compact;

      reconsider Q9 = Q as non empty Subset of M by TOPMETR: 12;

      X is bounded_above

      proof

        take r = ( max_dist_max (P,Q));

        let p be ExtReal;

        assume p in X;

        then

        consider z be object 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 as Point of M;

        (( dist_max P) . z) <= r by A2, A3, Th23;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: HAUSDORF:25

    

     Th25: for M be non empty MetrSpace, P,Q be non empty Subset of ( TopSpaceMetr M), X be 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, P,Q be non empty Subset of ( TopSpaceMetr M), X be Subset of REAL ;

      assume that

       A1: X = (( dist_min P) .: Q) and

       A2: P is compact & Q is compact;

      reconsider Q9 = Q as non empty Subset of M by TOPMETR: 12;

      X is bounded_above

      proof

        take r = ( max_dist_max (P,Q));

        let p be ExtReal;

        assume p in X;

        then

        consider z be object 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 as Point of M;

        (( dist_min P) . z) <= r by A2, A3, Th22;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: HAUSDORF:26

    for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), z be Point of M st P is compact holds (( dist_min P) . z) <= (( dist_max P) . z)

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M), z be Point of M;

      consider w be Point of M such that

       A1: w in P and

       A2: (( dist_min P) . z) <= ( dist (w,z)) by Th19;

      assume P is compact;

      then (( dist_max P) . z) >= ( dist (z,w)) by A1, Th20;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: HAUSDORF:27

    

     Th27: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M) holds (( dist_min P) .: P) = { 0 }

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M);

      consider x be object such that

       A1: x in P by XBOOLE_0:def 1;

      thus (( dist_min P) .: P) c= { 0 }

      proof

        let y be object;

        assume y in (( dist_min P) .: P);

        then ex x be object 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 thesis by TARSKI:def 1;

      end;

      let y be object;

      

       A2: ( dom ( dist_min P)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

      assume y in { 0 };

      then y = 0 by TARSKI:def 1;

      then y = (( dist_min P) . x) by A1, Th5;

      hence thesis by A1, A2, FUNCT_1:def 6;

    end;

    theorem :: HAUSDORF:28

    

     Th28: for M be non empty MetrSpace, P,Q be 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, P,Q be non empty Subset of ( TopSpaceMetr M);

      assume P is compact & Q is compact;

      then ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( max_dist_min (P,Q)) by WEIERSTR: 32;

      hence thesis by METRIC_1: 5;

    end;

    theorem :: HAUSDORF:29

    

     Th29: for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M) holds ( max_dist_min (P,P)) = 0

    proof

      let M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M);

      

       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 thesis by SEQ_4: 9;

    end;

    theorem :: HAUSDORF:30

    for M be non empty MetrSpace, P,Q be 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, P,Q be non empty Subset of ( TopSpaceMetr M);

      assume P is compact & Q is compact;

      then ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( min_dist_max (P,Q)) by WEIERSTR: 31;

      hence thesis by METRIC_1: 5;

    end;

    theorem :: HAUSDORF:31

    

     Th31: for M be non empty MetrSpace, Q,R be non empty Subset of ( TopSpaceMetr M), y be 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, Q,R be non empty Subset of ( TopSpaceMetr M), y be Point of M;

      assume that

       A1: Q is compact & R is compact and

       A2: y in Q;

      set A = (( dist_min R) .: Q);

      consider X be non empty Subset of REAL such that

       A3: A = X and

       A4: ( upper_bound A) = ( 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 thesis by A4, A5, SEQ_4:def 1;

    end;

    begin

    definition

      let M be non empty MetrSpace, P,Q be Subset of ( TopSpaceMetr M);

      :: HAUSDORF:def1

      func HausDist (P,Q) -> Real equals ( max (( max_dist_min (P,Q)),( max_dist_min (Q,P))));

      coherence ;

      commutativity ;

    end

    theorem :: HAUSDORF:32

    

     Th32: for M be non empty MetrSpace, Q,R be non empty Subset of ( TopSpaceMetr M), y be 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, Q,R be non empty Subset of ( TopSpaceMetr M), y be Point of M;

      assume Q is compact & R is compact & y in Q;

      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 thesis by XXREAL_0: 2;

    end;

    theorem :: HAUSDORF:33

    

     Th33: for M be non empty MetrSpace, P,Q,R be 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, P,Q,R be non empty Subset of ( TopSpaceMetr M);

      assume that

       A1: P is compact and

       A2: Q is compact and

       A3: R is compact;

      reconsider DPR = (( dist_min P) .: R) as non empty Subset of REAL by TOPMETR: 17;

      

       A4: for w be Real st w in DPR holds w <= (( HausDist (P,Q)) + ( HausDist (Q,R)))

      proof

        let w be Real;

        assume w in DPR;

        then

        consider y be object 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 as Point of M by A5, TOPMETR: 12;

        for z be 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;

          assume z in Q;

          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 thesis by XREAL_1: 20;

        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 thesis by A6, A8, XXREAL_0: 2;

      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 thesis by A4, SEQ_4: 45;

    end;

    theorem :: HAUSDORF:34

    for M be non empty MetrSpace, P,Q,R be 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, P,Q,R be non empty Subset of ( TopSpaceMetr M);

      assume that

       A1: P is compact and

       A2: Q is compact and

       A3: R is compact;

      reconsider DPR = (( dist_min R) .: P) as non empty Subset of REAL by TOPMETR: 17;

      

       A4: for w be Real st w in DPR holds w <= (( HausDist (P,Q)) + ( HausDist (Q,R)))

      proof

        let w be Real;

        assume w in DPR;

        then

        consider y be object 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 as Point of M by A5, TOPMETR: 12;

        for z be 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;

          assume z in Q;

          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 thesis by XREAL_1: 20;

        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 thesis by A6, XREAL_1: 20;

      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 thesis by A4, SEQ_4: 45;

    end;

    theorem :: HAUSDORF:35

    

     Th35: for M be non empty MetrSpace, P,Q be 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, P,Q be non empty Subset of ( TopSpaceMetr M);

      assume

       A1: P is compact & Q is compact;

      per cases by XXREAL_0: 16;

        suppose ( HausDist (P,Q)) = ( max_dist_min (P,Q));

        hence thesis by A1, Th28;

      end;

        suppose ( HausDist (P,Q)) = ( max_dist_min (Q,P));

        hence thesis by A1, Th28;

      end;

    end;

    theorem :: HAUSDORF:36

    for M be non empty MetrSpace, P be non empty Subset of ( TopSpaceMetr M) holds ( HausDist (P,P)) = 0 by Th29;

    theorem :: HAUSDORF:37

    

     Th37: for M be non empty MetrSpace, P,Q be 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, P,Q be non empty Subset of ( TopSpaceMetr M);

      assume that

       A1: P is compact and

       A2: Q is compact;

      

       A3: Q is closed by A2, COMPTS_1: 7;

      assume

       A4: ( HausDist (P,Q)) = 0 ;

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

      proof

        let x be object;

        assume

         A8: x in P;

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

      end;

      let x be object;

      assume

       A10: x in Q;

      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 be 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 thesis;

    end;

    theorem :: HAUSDORF:38

    

     Th38: for M be non empty MetrSpace, P,Q,R be 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, P,Q,R be non empty Subset of ( TopSpaceMetr M);

      assume P is compact & Q is compact & R is compact;

      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 thesis by XXREAL_0: 28;

    end;

    definition

      let n be Element of NAT ;

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

      :: HAUSDORF:def2

      func max_dist_min (P,Q) -> Real means ex P9,Q9 be Subset of ( TopSpaceMetr ( Euclid n)) st P = P9 & Q = Q9 & it = ( max_dist_min (P9,Q9));

      existence

      proof

         the TopStruct 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)), P9, Q9;

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let n be Element of NAT ;

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

      :: HAUSDORF:def3

      func HausDist (P,Q) -> Real means

      : Def3: ex P9,Q9 be Subset of ( TopSpaceMetr ( Euclid n)) st P = P9 & Q = Q9 & it = ( HausDist (P9,Q9));

      existence

      proof

         the TopStruct 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)), P9, Q9;

        thus thesis;

      end;

      uniqueness ;

      commutativity ;

    end

    reserve n for Element of NAT ;

    theorem :: HAUSDORF:39

    for P,Q be non empty Subset of ( TOP-REAL n) st P is compact & Q is compact holds ( HausDist (P,Q)) >= 0

    proof

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

      

       A1: the TopStruct 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;

      then P1 is compact & Q1 is compact by A1, COMPTS_1: 23;

      then ( HausDist (P1,Q1)) >= 0 by Th35;

      hence thesis by Def3;

    end;

    theorem :: HAUSDORF:40

    for P be non empty Subset of ( TOP-REAL n) holds ( HausDist (P,P)) = 0

    proof

      let P be non empty Subset of ( TOP-REAL n);

       the TopStruct 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 thesis by Def3;

    end;

    theorem :: HAUSDORF:41

    for P,Q be non empty Subset of ( TOP-REAL n) st P is compact & Q is compact & ( HausDist (P,Q)) = 0 holds P = Q

    proof

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

      assume that

       A1: P is compact & Q is compact and

       A2: ( HausDist (P,Q)) = 0 ;

      

       A3: the TopStruct 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 thesis by A4, Th37;

    end;

    theorem :: HAUSDORF:42

    for P,Q,R be 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 P,Q,R be non empty Subset of ( TOP-REAL n);

      assume that

       A1: P is compact & Q is compact and

       A2: R is compact;

      

       A3: the TopStruct 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 thesis by A4, A6, A5, Th38;

    end;