jordan1k.miz



    begin

    reserve X for set,

Y for non empty set;

    theorem :: JORDAN1K:1

    

     Th1: for f be Function of X, Y st f is onto holds for y be Element of Y holds ex x be object st x in X & y = (f . x) by FUNCT_2: 11;

    theorem :: JORDAN1K:2

    for f be Function of X, Y st f is onto holds for y be Element of Y holds ex x be Element of X st y = (f . x)

    proof

      let f be Function of X, Y such that

       A1: f is onto;

      let y be Element of Y;

      ex x be object st x in X & (f . x) = y by A1, Th1;

      hence thesis;

    end;

    theorem :: JORDAN1K:3

    

     Th3: for f be Function of X, Y, A be Subset of X st f is onto holds ((f .: A) ` ) c= (f .: (A ` ))

    proof

      let f be Function of X, Y, A be Subset of X such that

       A1: f is onto;

      let e be object;

      assume

       A2: e in ((f .: A) ` );

      then

      reconsider y = e as Element of Y;

      consider u be object such that

       A3: u in X and

       A4: y = (f . u) by A1, Th1;

      reconsider x = u as Element of X by A3;

      now

        assume x in A;

        then y in (f .: A) by A4, FUNCT_2: 35;

        hence contradiction by A2, XBOOLE_0:def 5;

      end;

      then x in (A ` ) by A3, SUBSET_1: 29;

      hence thesis by A4, FUNCT_2: 35;

    end;

    theorem :: JORDAN1K:4

    

     Th4: for f be Function of X, Y, A be Subset of X st f is one-to-one holds (f .: (A ` )) c= ((f .: A) ` )

    proof

      let f be Function of X, Y, A be Subset of X such that

       A1: f is one-to-one;

      let e be object;

      assume

       A2: e in (f .: (A ` ));

      then

      reconsider y = e as Element of Y;

      consider x1 be object such that

       A3: x1 in X and

       A4: x1 in (A ` ) and

       A5: y = (f . x1) by A2, FUNCT_2: 64;

      assume not e in ((f .: A) ` );

      then

       A6: ex x2 be object st x2 in X & x2 in A & y = (f . x2) by FUNCT_2: 64, SUBSET_1: 29;

       not x1 in A by A4, XBOOLE_0:def 5;

      hence contradiction by A1, A3, A5, A6, FUNCT_2: 19;

    end;

    theorem :: JORDAN1K:5

    

     Th5: for f be Function of X, Y, A be Subset of X st f is bijective holds ((f .: A) ` ) = (f .: (A ` )) by Th3, Th4;

    begin

    theorem :: JORDAN1K:6

    

     Th6: for T be TopSpace holds for A be Subset of T holds A is_a_component_of ( {} T) iff A is empty

    proof

      let T be TopSpace;

      let A be Subset of T;

      thus A is_a_component_of ( {} T) implies A is empty by SPRECT_1: 5, XBOOLE_1: 3;

      assume

       A1: A is empty;

      then

      reconsider B = A as Subset of (T | ( {} T)) by XBOOLE_1: 2;

      for C be Subset of (T | ( {} T)) st C is connected holds B c= C implies B = C by A1;

      then B is a_component by A1, CONNSP_1:def 5;

      hence thesis by CONNSP_1:def 6;

    end;

    theorem :: JORDAN1K:7

    

     Th7: for T be non empty TopSpace holds for A,B,C be Subset of T st A c= B & A is_a_component_of C & B is_a_component_of C holds A = B

    proof

      let T be non empty TopSpace;

      let A,B,C be Subset of T such that

       A1: A c= B and

       A2: A is_a_component_of C and

       A3: B is_a_component_of C;

      per cases ;

        suppose C = {} ;

        then

         A4: C = ( {} T);

        then A = {} by A2, Th6;

        hence thesis by A3, A4, Th6;

      end;

        suppose C is non empty;

        then A <> {} by A2, SPRECT_1: 4;

        hence thesis by A1, A2, A3, GOBOARD9: 1, XBOOLE_1: 69;

      end;

    end;

    reserve n for Nat;

    theorem :: JORDAN1K:8

    n >= 1 implies for P be Subset of ( Euclid n) holds P is bounded implies not (P ` ) is bounded

    proof

      assume

       A1: n >= 1;

      ( REAL n) c= the carrier of ( Euclid n);

      then

      reconsider W = ( REAL n) as Subset of ( Euclid n);

      let P be Subset of ( Euclid n);

      

       A2: (P \/ (P ` )) = ( [#] ( Euclid n)) by PRE_TOPC: 2

      .= W;

      assume P is bounded & (P ` ) is bounded;

      hence contradiction by A1, A2, JORDAN2C: 33, TBSP_1: 13;

    end;

    reserve r for Real,

M for non empty MetrSpace;

    theorem :: JORDAN1K:9

    

     Th9: for C be non empty Subset of ( TopSpaceMetr M), p be Point of ( TopSpaceMetr M) holds (( dist_min C) . p) >= 0

    proof

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

      

       A1: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x = p as Point of M;

      set B = ( [#] (( dist x) .: C));

      

       A2: B = (( dist x) .: C) by WEIERSTR:def 1;

      

       A3: for r be Real st r in B holds 0 <= r

      proof

        let r be Real;

        assume r in B;

        then

        consider y be object such that y in ( dom ( dist x)) and

         A4: y in C and

         A5: r = (( dist x) . y) by A2, FUNCT_1:def 6;

        reconsider y9 = y as Point of M by A1, A4;

        r = ( dist (x,y9)) by A5, WEIERSTR:def 4;

        hence thesis by METRIC_1: 5;

      end;

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

      then ( lower_bound B) >= 0 by A2, A3, SEQ_4: 43;

      then ( lower_bound (( dist x) .: C)) >= 0 by WEIERSTR:def 3;

      hence thesis by WEIERSTR:def 6;

    end;

    theorem :: JORDAN1K:10

    

     Th10: for C be non empty Subset of ( TopSpaceMetr M), p be Point of M st for q be Point of M st q in C holds ( dist (p,q)) >= r holds (( dist_min C) . p) >= r

    proof

      let C be non empty Subset of ( TopSpaceMetr M), p be Point of M such that

       A1: for q be Point of M st q in C holds ( dist (p,q)) >= r;

      set B = ( [#] (( dist p) .: C));

      

       A2: B = (( dist p) .: C) by WEIERSTR:def 1;

      

       A3: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      

       A4: for s be Real st s in B holds r <= s

      proof

        let s be Real;

        assume s in B;

        then

        consider y be object such that y in ( dom ( dist p)) and

         A5: y in C and

         A6: s = (( dist p) . y) by A2, FUNCT_1:def 6;

        reconsider y9 = y as Point of M by A3, A5;

        s = ( dist (p,y9)) by A6, WEIERSTR:def 4;

        hence thesis by A1, A5;

      end;

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

      then ( lower_bound B) >= r by A2, A4, SEQ_4: 43;

      then ( lower_bound (( dist p) .: C)) >= r by WEIERSTR:def 3;

      hence thesis by WEIERSTR:def 6;

    end;

    theorem :: JORDAN1K:11

    

     Th11: for A,B be non empty Subset of ( TopSpaceMetr M) holds ( min_dist_min (A,B)) >= 0

    proof

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

      set X = ( [#] (( dist_min A) .: B));

      

       A1: X = (( dist_min A) .: B) by WEIERSTR:def 1;

      

       A2: for r be Real st r in X holds 0 <= r

      proof

        let r be Real;

        assume r in X;

        then

        consider y be object such that y in ( dom ( dist_min A)) and

         A3: y in B and

         A4: r = (( dist_min A) . y) by A1, FUNCT_1:def 6;

        reconsider y as Point of ( TopSpaceMetr M) by A3;

        (( dist_min A) . y) >= 0 by Th9;

        hence thesis by A4;

      end;

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

      then ( lower_bound X) >= 0 by A1, A2, SEQ_4: 43;

      then ( lower_bound (( dist_min A) .: B)) >= 0 by WEIERSTR:def 3;

      hence thesis by WEIERSTR:def 7;

    end;

    theorem :: JORDAN1K:12

    

     Th12: for A,B be compact Subset of ( TopSpaceMetr M) st A meets B holds ( min_dist_min (A,B)) = 0

    proof

      let A,B be compact Subset of ( TopSpaceMetr M);

      assume A meets B;

      then

      consider p be object such that

       A1: p in A and

       A2: p in B by XBOOLE_0: 3;

      ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider p as Point of M by A1;

      ( min_dist_min (A,B)) >= 0 & ( min_dist_min (A,B)) <= ( dist (p,p)) by A1, A2, Th11, WEIERSTR: 34;

      hence thesis by METRIC_1: 1;

    end;

    theorem :: JORDAN1K:13

    

     Th13: for A,B be non empty Subset of ( TopSpaceMetr M) st for p,q be Point of M st p in A & q in B holds ( dist (p,q)) >= r holds ( min_dist_min (A,B)) >= r

    proof

      let A,B be non empty Subset of ( TopSpaceMetr M) such that

       A1: for p,q be Point of M st p in A & q in B holds ( dist (p,q)) >= r;

      set X = ( [#] (( dist_min A) .: B));

      

       A2: X = (( dist_min A) .: B) by WEIERSTR:def 1;

      

       A3: for s be Real st s in X holds r <= s

      proof

        let s be Real;

        assume s in X;

        then

        consider y be object such that y in ( dom ( dist_min A)) and

         A4: y in B and

         A5: s = (( dist_min A) . y) by A2, FUNCT_1:def 6;

        reconsider y as Point of ( TopSpaceMetr M) by A4;

        reconsider p = y as Point of M by TOPMETR: 12;

        for q be Point of M st q in A holds ( dist (p,q)) >= r by A1, A4;

        hence thesis by A5, Th10;

      end;

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

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

      then ( lower_bound (( dist_min A) .: B)) >= r by WEIERSTR:def 3;

      hence thesis by WEIERSTR:def 7;

    end;

    begin

    theorem :: JORDAN1K:14

    

     Th14: for P,Q be Subset of ( TOP-REAL n) st P is_a_component_of (Q ` ) holds P is_inside_component_of Q or P is_outside_component_of Q by JORDAN2C:def 2, JORDAN2C:def 3;

    theorem :: JORDAN1K:15

    n >= 1 implies ( BDD ( {} ( TOP-REAL n))) = ( {} ( TOP-REAL n))

    proof

      set X = { B where B be Subset of ( TOP-REAL n) : B is_inside_component_of ( {} ( TOP-REAL n)) };

      assume n >= 1;

      then

       A1: not ( [#] ( TOP-REAL n)) is bounded by JORDAN2C: 35;

      now

        ( [#] ( TOP-REAL n)) is a_component;

        then

         A2: ( [#] the TopStruct of ( TOP-REAL n)) is a_component by CONNSP_1: 45;

        (( TOP-REAL n) | ( [#] ( TOP-REAL n))) = the TopStruct of ( TOP-REAL n) by TSEP_1: 93;

        then

         A3: ( [#] ( TOP-REAL n)) is_a_component_of ( [#] ( TOP-REAL n)) by A2, CONNSP_1:def 6;

        assume X <> {} ;

        then

        consider x be object such that

         A4: x in X by XBOOLE_0:def 1;

        consider B be Subset of ( TOP-REAL n) such that x = B and

         A5: B is_inside_component_of ( {} ( TOP-REAL n)) by A4;

        B is_a_component_of (( {} ( TOP-REAL n)) ` ) by A5, JORDAN2C:def 2;

        then B = ( [#] ( TOP-REAL n)) by A3, Th7;

        hence contradiction by A1, A5, JORDAN2C:def 2;

      end;

      hence thesis by JORDAN2C:def 4, ZFMISC_1: 2;

    end;

    theorem :: JORDAN1K:16

    ( BDD ( [#] ( TOP-REAL n))) = ( {} ( TOP-REAL n))

    proof

      ( BDD ( [#] ( TOP-REAL n))) c= (( [#] ( TOP-REAL n)) ` ) by JORDAN2C: 25;

      then ( BDD ( [#] ( TOP-REAL n))) c= ( {} ( TOP-REAL n)) by XBOOLE_1: 37;

      hence thesis by XBOOLE_1: 3;

    end;

    theorem :: JORDAN1K:17

    n >= 1 implies ( UBD ( {} ( TOP-REAL n))) = ( [#] ( TOP-REAL n))

    proof

      set X = { B where B be Subset of ( TOP-REAL n) : B is_outside_component_of ( {} ( TOP-REAL n)) };

      assume n >= 1;

      then

       A1: not ( [#] ( TOP-REAL n)) is bounded by JORDAN2C: 35;

      thus ( UBD ( {} ( TOP-REAL n))) c= ( [#] ( TOP-REAL n));

      ( [#] ( TOP-REAL n)) is a_component;

      then

       A2: ( [#] the TopStruct of ( TOP-REAL n)) is a_component by CONNSP_1: 45;

      (( TOP-REAL n) | ( [#] ( TOP-REAL n))) = the TopStruct of ( TOP-REAL n) by TSEP_1: 93;

      then

       A3: ( [#] ( TOP-REAL n)) is_a_component_of ( [#] ( TOP-REAL n)) by A2, CONNSP_1:def 6;

      ( [#] ( TOP-REAL n)) = (( {} ( TOP-REAL n)) ` );

      then ( [#] ( TOP-REAL n)) is_outside_component_of ( {} ( TOP-REAL n)) by A1, A3, JORDAN2C:def 3;

      then ( [#] ( TOP-REAL n)) in X;

      then ( [#] ( TOP-REAL n)) c= ( union X) by ZFMISC_1: 74;

      hence thesis by JORDAN2C:def 5;

    end;

    theorem :: JORDAN1K:18

    ( UBD ( [#] ( TOP-REAL n))) = ( {} ( TOP-REAL n))

    proof

      ( UBD ( [#] ( TOP-REAL n))) c= (( [#] ( TOP-REAL n)) ` ) by JORDAN2C: 26;

      then ( UBD ( [#] ( TOP-REAL n))) c= ( {} ( TOP-REAL n)) by XBOOLE_1: 37;

      hence thesis by XBOOLE_1: 3;

    end;

    theorem :: JORDAN1K:19

    for P be connected Subset of ( TOP-REAL n), Q be Subset of ( TOP-REAL n) st P misses Q holds P c= ( UBD Q) or P c= ( BDD Q)

    proof

      let P be connected Subset of ( TOP-REAL n), Q be Subset of ( TOP-REAL n) such that

       A1: P misses Q;

      per cases ;

        suppose P is empty;

        hence thesis;

      end;

        suppose Q = ( [#] ( TOP-REAL n));

        then P = {} by A1, XBOOLE_1: 67;

        hence thesis;

      end;

        suppose that

         A2: not P is empty and Q <> ( [#] ( TOP-REAL n));

        P c= (Q ` ) by A1, SUBSET_1: 23;

        then

        consider C be Subset of ( TOP-REAL n) such that

         A3: C is_a_component_of (Q ` ) and

         A4: P c= C by A2, GOBOARD9: 3;

        C is_inside_component_of Q or C is_outside_component_of Q by A3, Th14;

        then C c= ( UBD Q) or C c= ( BDD Q) by JORDAN2C: 22, JORDAN2C: 23;

        hence thesis by A4;

      end;

    end;

    begin

    reserve n for Nat,

p,q,q1,q2 for Point of ( TOP-REAL 2),

r,s1,s2,t1,t2 for Real,

x,y for Point of ( Euclid 2);

    theorem :: JORDAN1K:20

    

     Th20: ( dist ( |[ 0 , 0 ]|,(r * q))) = ( |.r.| * ( dist ( |[ 0 , 0 ]|,q)))

    proof

      

       A1: (r ^2 ) >= 0 & ((q `1 ) ^2 ) >= 0 by XREAL_1: 63;

      

       A2: ((q `2 ) ^2 ) >= 0 by XREAL_1: 63;

      

       A3: ( |[ 0 , 0 ]| `1 ) = 0 & ( |[ 0 , 0 ]| `2 ) = 0 by EUCLID: 52;

      

      then

       A4: ( dist ( |[ 0 , 0 ]|,q)) = ( sqrt ((( 0 - (q `1 )) ^2 ) + (( 0 - (q `2 )) ^2 ))) by TOPREAL6: 92

      .= ( sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 )));

      

      thus ( dist ( |[ 0 , 0 ]|,(r * q))) = ( sqrt ((( 0 - ((r * q) `1 )) ^2 ) + (( 0 - ((r * q) `2 )) ^2 ))) by A3, TOPREAL6: 92

      .= ( sqrt ((((r * q) `1 ) ^2 ) + (( - ((r * q) `2 )) ^2 )))

      .= ( sqrt (((r * (q `1 )) ^2 ) + (((r * q) `2 ) ^2 ))) by TOPREAL3: 4

      .= ( sqrt (((r ^2 ) * ((q `1 ) ^2 )) + ((r * (q `2 )) ^2 ))) by TOPREAL3: 4

      .= ( sqrt ((r ^2 ) * (((q `1 ) ^2 ) + ((q `2 ) ^2 ))))

      .= (( sqrt (r ^2 )) * ( sqrt (((q `1 ) ^2 ) + ((q `2 ) ^2 )))) by A1, A2, SQUARE_1: 29

      .= ( |.r.| * ( dist ( |[ 0 , 0 ]|,q))) by A4, COMPLEX1: 72;

    end;

    theorem :: JORDAN1K:21

    

     Th21: ( dist ((q1 + q),(q2 + q))) = ( dist (q1,q2))

    proof

      

       A1: (((q1 + q) `1 ) - ((q2 + q) `1 )) = (((q1 `1 ) + (q `1 )) - ((q2 + q) `1 )) by TOPREAL3: 2

      .= (((q1 `1 ) + (q `1 )) - ((q2 `1 ) + (q `1 ))) by TOPREAL3: 2

      .= (((q1 `1 ) - (q2 `1 )) + 0 );

      

       A2: (((q1 + q) `2 ) - ((q2 + q) `2 )) = (((q1 `2 ) + (q `2 )) - ((q2 + q) `2 )) by TOPREAL3: 2

      .= (((q1 `2 ) + (q `2 )) - ((q2 `2 ) + (q `2 ))) by TOPREAL3: 2

      .= (((q1 `2 ) - (q2 `2 )) + 0 );

      

      thus ( dist ((q1 + q),(q2 + q))) = ( sqrt (((((q1 + q) `1 ) - ((q2 + q) `1 )) ^2 ) + ((((q1 + q) `2 ) - ((q2 + q) `2 )) ^2 ))) by TOPREAL6: 92

      .= ( dist (q1,q2)) by A1, A2, TOPREAL6: 92;

    end;

    theorem :: JORDAN1K:22

    

     Th22: p <> q implies ( dist (p,q)) > 0

    proof

      ex p9,q9 be Point of ( Euclid 2) st p9 = p & q9 = q & ( dist (p,q)) = ( dist (p9,q9)) by TOPREAL6:def 1;

      hence thesis by METRIC_1: 7;

    end;

    theorem :: JORDAN1K:23

    

     Th23: ( dist ((q1 - q),(q2 - q))) = ( dist (q1,q2)) by Th21;

    theorem :: JORDAN1K:24

    

     Th24: ( dist (p,q)) = ( dist (( - p),( - q)))

    proof

      

      thus ( dist (p,q)) = ( dist ((q - q),(p - q))) by Th23

      .= ( dist ((q - q),(p + ( - q))))

      .= ( dist ( |[ 0 , 0 ]|,(p + ( - q)))) by EUCLID: 54, RLVECT_1: 5

      .= ( dist ((p - p),(p + ( - q)))) by EUCLID: 54, RLVECT_1: 5

      .= ( dist ((p + ( - p)),(p + ( - q))))

      .= ( dist (( - p),( - q))) by Th21;

    end;

    theorem :: JORDAN1K:25

    

     Th25: ( dist ((q - q1),(q - q2))) = ( dist (q1,q2))

    proof

      ( - (q - q1)) = (q1 - q) & ( - (q - q2)) = (q2 - q) by RLVECT_1: 33;

      

      hence ( dist ((q - q1),(q - q2))) = ( dist ((q1 - q),(q2 - q))) by Th24

      .= ( dist (q1,q2)) by Th23;

    end;

    theorem :: JORDAN1K:26

    

     Th26: ( dist ((r * p),(r * q))) = ( |.r.| * ( dist (p,q)))

    proof

      

      thus ( dist ((r * p),(r * q))) = ( dist (((r * p) - (r * p)),((r * p) - (r * q)))) by Th25

      .= ( dist ( |[ 0 , 0 ]|,((r * p) - (r * q)))) by EUCLID: 54, RLVECT_1: 5

      .= ( dist ( |[ 0 , 0 ]|,(r * (p - q)))) by RLVECT_1: 34

      .= ( |.r.| * ( dist ( |[ 0 , 0 ]|,(p - q)))) by Th20

      .= ( |.r.| * ( dist ((p - p),(p - q)))) by EUCLID: 54, RLVECT_1: 5

      .= ( |.r.| * ( dist (p,q))) by Th25;

    end;

    theorem :: JORDAN1K:27

    

     Th27: r <= 1 implies ( dist (p,((r * p) + ((1 - r) * q)))) = ((1 - r) * ( dist (p,q)))

    proof

      assume r <= 1;

      then (1 + r) <= (1 + 1) by XREAL_1: 6;

      then (1 - r) >= (1 - 1) by XREAL_1: 21;

      then

       A1: |.(1 - r).| = (1 - r) by ABSVALUE:def 1;

      

      thus ( dist (p,((r * p) + ((1 - r) * q)))) = ( dist (((r + (1 - r)) * p),((r * p) + ((1 - r) * q)))) by RLVECT_1:def 8

      .= ( dist (((r * p) + ((1 - r) * p)),((r * p) + ((1 - r) * q)))) by RLVECT_1:def 6

      .= ( dist (((1 - r) * p),((1 - r) * q))) by Th21

      .= ((1 - r) * ( dist (p,q))) by A1, Th26;

    end;

    theorem :: JORDAN1K:28

    

     Th28: 0 <= r implies ( dist (q,((r * p) + ((1 - r) * q)))) = (r * ( dist (p,q)))

    proof

      assume 0 <= r;

      then

       A1: |.r.| = r by ABSVALUE:def 1;

      

      thus ( dist (q,((r * p) + ((1 - r) * q)))) = ( dist (((r * p) + ((1 - r) * q)),((r + (1 - r)) * q))) by RLVECT_1:def 8

      .= ( dist (((r * q) + ((1 - r) * q)),((r * p) + ((1 - r) * q)))) by RLVECT_1:def 6

      .= ( dist ((r * q),(r * p))) by Th21

      .= (r * ( dist (p,q))) by A1, Th26;

    end;

    theorem :: JORDAN1K:29

    

     Th29: p in ( LSeg (q1,q2)) implies (( dist (q1,p)) + ( dist (p,q2))) = ( dist (q1,q2))

    proof

      assume p in ( LSeg (q1,q2));

      then

      consider r such that

       A1: p = (((1 - r) * q1) + (r * q2)) & 0 <= r & r <= 1;

      ( dist (q1,p)) = (r * ( dist (q1,q2))) & ( dist (q2,p)) = ((1 - r) * ( dist (q1,q2))) by A1, Th27, Th28;

      hence thesis;

    end;

    theorem :: JORDAN1K:30

    q1 in ( LSeg (q2,p)) & q1 <> q2 implies ( dist (q1,p)) < ( dist (q2,p))

    proof

      assume that

       A1: q1 in ( LSeg (q2,p)) and

       A2: q1 <> q2;

      (( dist (q2,q1)) + ( dist (q1,p))) = ( dist (q2,p)) by A1, Th29;

      hence thesis by A2, Th22, XREAL_1: 29;

    end;

    theorem :: JORDAN1K:31

    

     Th31: y = |[ 0 , 0 ]| implies ( Ball (y,r)) = { q : |.q.| < r }

    proof

      set X = { q : |.( |[ 0 , 0 ]| - q).| < r }, Y = { q : |.q.| < r };

      

       A1: X c= Y

      proof

        let u be object;

        assume u in X;

        then

        consider q such that

         A2: u = q & |.( |[ 0 , 0 ]| - q).| < r;

         |.( |[ 0 , 0 ]| - q).| = |.(q - |[ 0 , 0 ]|).| by TOPRNS_1: 27

        .= |.q.| by EUCLID: 54, RLVECT_1: 13;

        hence thesis by A2;

      end;

      

       A3: Y c= X

      proof

        let u be object;

        assume u in Y;

        then

        consider q such that

         A4: u = q & |.q.| < r;

         |.( |[ 0 , 0 ]| - q).| = |.(q - |[ 0 , 0 ]|).| by TOPRNS_1: 27

        .= |.q.| by EUCLID: 54, RLVECT_1: 13;

        hence thesis by A4;

      end;

      assume y = |[ 0 , 0 ]|;

      

      hence ( Ball (y,r)) = { q : |.( |[ 0 , 0 ]| - q).| < r } by JGRAPH_2: 2

      .= { q : |.q.| < r } by A1, A3;

    end;

    begin

    theorem :: JORDAN1K:32

    

     Th32: (( AffineMap (r,s1,r,s2)) . p) = ((r * p) + |[s1, s2]|)

    proof

      

      thus (( AffineMap (r,s1,r,s2)) . p) = |[((r * (p `1 )) + s1), ((r * (p `2 )) + s2)]| by JGRAPH_2:def 2

      .= |[(((r * p) `1 ) + s1), ((r * (p `2 )) + s2)]| by TOPREAL3: 4

      .= |[(((r * p) `1 ) + s1), (((r * p) `2 ) + s2)]| by TOPREAL3: 4

      .= ( |[((r * p) `1 ), ((r * p) `2 )]| + |[s1, s2]|) by EUCLID: 56

      .= ((r * p) + |[s1, s2]|) by EUCLID: 53;

    end;

    theorem :: JORDAN1K:33

    

     Th33: (( AffineMap (r,(q `1 ),r,(q `2 ))) . p) = ((r * p) + q)

    proof

      

      thus (( AffineMap (r,(q `1 ),r,(q `2 ))) . p) = ((r * p) + |[(q `1 ), (q `2 )]|) by Th32

      .= ((r * p) + q) by EUCLID: 53;

    end;

    theorem :: JORDAN1K:34

    

     Th34: s1 > 0 & s2 > 0 implies (( AffineMap (s1,t1,s2,t2)) * ( AffineMap ((1 / s1),( - (t1 / s1)),(1 / s2),( - (t2 / s2))))) = ( id ( REAL 2))

    proof

      the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

      then

      reconsider f = ( id ( REAL 2)) as Function of the carrier of ( TOP-REAL 2), the carrier of ( TOP-REAL 2);

      assume that

       A1: s1 > 0 and

       A2: s2 > 0 ;

      now

        let p be Point of ( TOP-REAL 2);

        set q = |[(((1 / s1) * (p `1 )) - (t1 / s1)), (((1 / s2) * (p `2 )) - (t2 / s2))]|;

        

         A3: (q `2 ) = (((1 / s2) * (p `2 )) - (t2 / s2)) by EUCLID: 52;

        p in the carrier of ( TOP-REAL 2);

        then

         A4: p in ( REAL 2) by EUCLID: 22;

        

         A5: (s1 * (1 / s1)) = 1 by A1, XCMPLX_1: 106;

        

        thus ((( AffineMap (s1,t1,s2,t2)) * ( AffineMap ((1 / s1),( - (t1 / s1)),(1 / s2),( - (t2 / s2))))) . p) = (( AffineMap (s1,t1,s2,t2)) . (( AffineMap ((1 / s1),( - (t1 / s1)),(1 / s2),( - (t2 / s2)))) . p)) by FUNCT_2: 15

        .= (( AffineMap (s1,t1,s2,t2)) . |[(((1 / s1) * (p `1 )) + ( - (t1 / s1))), (((1 / s2) * (p `2 )) + ( - (t2 / s2)))]|) by JGRAPH_2:def 2

        .= |[((s1 * (q `1 )) + t1), ((s2 * (q `2 )) + t2)]| by JGRAPH_2:def 2

        .= |[((s1 * (((1 / s1) * (p `1 )) - (t1 / s1))) + t1), ((s2 * (q `2 )) + t2)]| by EUCLID: 52

        .= |[((((s1 * (1 / s1)) * (p `1 )) - (s1 * (t1 / s1))) + t1), ((s2 * (q `2 )) + t2)]|

        .= |[(((1 * (p `1 )) - (1 * t1)) + t1), ((s2 * (q `2 )) + t2)]| by A1, A5, XCMPLX_1: 87

        .= |[(p `1 ), (((s2 * ((1 / s2) * (p `2 ))) - (s2 * (t2 / s2))) + t2)]| by A3

        .= |[(p `1 ), ((((s2 * (1 / s2)) * (p `2 )) - t2) + t2)]| by A2, XCMPLX_1: 87

        .= |[(p `1 ), (((1 * (p `2 )) - (1 * t2)) + t2)]| by A2, XCMPLX_1: 106

        .= p by EUCLID: 53

        .= (f . p) by A4, FUNCT_1: 18;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: JORDAN1K:35

    

     Th35: y = |[ 0 , 0 ]| & x = q & r > 0 implies (( AffineMap (r,(q `1 ),r,(q `2 ))) .: ( Ball (y,1))) = ( Ball (x,r))

    proof

      assume that

       A1: y = |[ 0 , 0 ]| and

       A2: x = q and

       A3: r > 0 ;

      reconsider A = ( Ball (y,1)), B = ( Ball (x,r)) as Subset of ( TOP-REAL 2) by TOPREAL3: 8;

      

       A4: B c= (( AffineMap (r,(q `1 ),r,(q `2 ))) .: A)

      proof

        let u be object;

        assume

         A5: u in B;

        then

        reconsider q1 = u as Point of ( TOP-REAL 2);

        reconsider x1 = q1 as Element of ( Euclid 2) by TOPREAL3: 8;

        set q2 = (( AffineMap ((1 / r),( - ((q `1 ) / r)),(1 / r),( - ((q `2 ) / r)))) . q1);

        consider z1,z2 be Point of ( Euclid 2) such that

         A6: z1 = q and

         A7: z2 = ((r * q2) + q) and

         A8: ( dist (q,((r * q2) + q))) = ( dist (z1,z2)) by TOPREAL6:def 1;

        consider z3,z4 be Point of ( Euclid 2) such that

         A9: z3 = |[ 0 , 0 ]| and

         A10: z4 = q2 and

         A11: ( dist ( |[ 0 , 0 ]|,q2)) = ( dist (z3,z4)) by TOPREAL6:def 1;

        z2 = (( AffineMap (r,(q `1 ),r,(q `2 ))) . q2) by A7, Th33

        .= ((( AffineMap (r,(q `1 ),r,(q `2 ))) * ( AffineMap ((1 / r),( - ((q `1 ) / r)),(1 / r),( - ((q `2 ) / r))))) . q1) by FUNCT_2: 15

        .= (( id ( REAL 2)) . q1) by A3, Th34

        .= x1;

        

        then ( dist (x,x1)) = ( dist (( |[ 0 , 0 ]| + q),((r * q2) + q))) by A2, A6, A8, EUCLID: 54, RLVECT_1: 4

        .= ( dist ( |[ 0 , 0 ]|,(r * q2))) by Th21

        .= ( |.r.| * ( dist ( |[ 0 , 0 ]|,q2))) by Th20

        .= (r * ( dist (y,z4))) by A1, A3, A9, A11, ABSVALUE:def 1;

        then (r * ( dist (y,z4))) < (1 * r) by A5, METRIC_1: 11;

        then ( dist (y,z4)) < 1 by A3, XREAL_1: 64;

        then

         A12: q2 in A by A10, METRIC_1: 11;

        (( AffineMap (r,(q `1 ),r,(q `2 ))) . q2) = ((( AffineMap (r,(q `1 ),r,(q `2 ))) * ( AffineMap ((1 / r),( - ((q `1 ) / r)),(1 / r),( - ((q `2 ) / r))))) . q1) by FUNCT_2: 15

        .= (( id ( REAL 2)) . q1) by A3, Th34

        .= (( id ( TOP-REAL 2)) . q1) by EUCLID: 22

        .= q1;

        hence thesis by A12, FUNCT_2: 35;

      end;

      (( AffineMap (r,(q `1 ),r,(q `2 ))) .: A) c= B

      proof

        let u be object;

        assume

         A13: u in (( AffineMap (r,(q `1 ),r,(q `2 ))) .: A);

        then

        reconsider q1 = u as Point of ( TOP-REAL 2);

        consider q2 such that

         A14: q2 in A and

         A15: q1 = (( AffineMap (r,(q `1 ),r,(q `2 ))) . q2) by A13, FUNCT_2: 65;

        reconsider x1 = q1, x2 = q2 as Element of ( Euclid 2) by TOPREAL3: 8;

        

         A16: ( dist (y,x2)) < 1 by A14, METRIC_1: 11;

        

         A17: ex z3,z4 be Point of ( Euclid 2) st z3 = |[ 0 , 0 ]| & z4 = q2 & ( dist ( |[ 0 , 0 ]|,q2)) = ( dist (z3,z4)) by TOPREAL6:def 1;

        

         A18: ex z1,z2 be Point of ( Euclid 2) st z1 = q & z2 = ((r * q2) + q) & ( dist (q,((r * q2) + q))) = ( dist (z1,z2)) by TOPREAL6:def 1;

        q1 = ((r * q2) + q) by A15, Th33;

        

        then ( dist (x,x1)) = ( dist (( |[ 0 , 0 ]| + q),((r * q2) + q))) by A2, A18, EUCLID: 54, RLVECT_1: 4

        .= ( dist ( |[ 0 , 0 ]|,(r * q2))) by Th21

        .= ( |.r.| * ( dist ( |[ 0 , 0 ]|,q2))) by Th20

        .= (r * ( dist (y,x2))) by A1, A3, A17, ABSVALUE:def 1;

        then ( dist (x,x1)) < r by A3, A16, XREAL_1: 157;

        hence thesis by METRIC_1: 11;

      end;

      hence thesis by A4;

    end;

    theorem :: JORDAN1K:36

    

     Th36: for A,B,C,D be Real st A > 0 & C > 0 holds ( AffineMap (A,B,C,D)) is onto

    proof

      let A,B,C,D be Real such that

       A1: A > 0 & C > 0 ;

      thus ( rng ( AffineMap (A,B,C,D))) c= the carrier of ( TOP-REAL 2);

      let e be object;

      assume e in the carrier of ( TOP-REAL 2);

      then

      reconsider q1 = e as Point of ( TOP-REAL 2);

      set q2 = (( AffineMap ((1 / A),( - (B / A)),(1 / C),( - (D / C)))) . q1);

      

       A2: the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

      (( AffineMap (A,B,C,D)) . q2) = ((( AffineMap (A,B,C,D)) * ( AffineMap ((1 / A),( - (B / A)),(1 / C),( - (D / C))))) . q1) by FUNCT_2: 15

      .= (( id ( REAL 2)) . q1) by A1, Th34

      .= q1 by A2;

      hence thesis by FUNCT_2: 4;

    end;

    theorem :: JORDAN1K:37

    (( Ball (x,r)) ` ) is connected Subset of ( TOP-REAL 2)

    proof

      set C = (( Ball (x,r)) ` );

      per cases ;

        suppose r <= 0 ;

        then ( Ball (x,r)) = ( {} ( TOP-REAL 2)) by TBSP_1: 12;

        then

         A1: C = ( [#] ( TOP-REAL 2)) by TOPREAL3: 8;

        thus thesis by A1;

      end;

        suppose

         A2: r > 0 ;

        reconsider q = x as Point of ( TOP-REAL 2) by TOPREAL3: 8;

        reconsider y = |[ 0 , 0 ]| as Point of ( Euclid 2) by TOPREAL3: 8;

        reconsider Q = ( Ball (x,r)), J = ( Ball (y,1)) as Subset of ( TOP-REAL 2) by TOPREAL3: 8;

        

         A3: Q = (( AffineMap (r,(q `1 ),r,(q `2 ))) .: J) by A2, Th35;

        reconsider P = (Q ` ), K = (J ` ) as Subset of ( TOP-REAL 2);

        

         A4: K = (( REAL 2) \ ( Ball (y,1))) by TOPREAL3: 8

        .= (( REAL 2) \ { q1 : |.q1.| < 1 }) by Th31;

        ( AffineMap (r,(q `1 ),r,(q `2 ))) is one-to-one & ( AffineMap (r,(q `1 ),r,(q `2 ))) is onto by A2, Th36, JGRAPH_2: 44;

        then the carrier of ( TOP-REAL 2) = the carrier of ( Euclid 2) & P = (( AffineMap (r,(q `1 ),r,(q `2 ))) .: K) by A3, Th5, TOPREAL3: 8;

        hence thesis by A4, JORDAN2C: 53, TOPS_2: 61;

      end;

    end;

    begin

    definition

      let n;

      let A,B be Subset of ( TOP-REAL n);

      :: JORDAN1K:def1

      func dist_min (A,B) -> Real means

      : Def1: ex A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) st A = A9 & B = B9 & it = ( min_dist_min (A9,B9));

      existence

      proof

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider A9 = A, B9 = B as Subset of ( TopSpaceMetr ( Euclid n));

        take ( min_dist_min (A9,B9)), A9, B9;

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let M be non empty MetrSpace;

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

      :: original: min_dist_min

      redefine

      func min_dist_min (P,Q);

      commutativity

      proof

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

        consider y1,y2 be Point of M such that

         A1: y1 in Q & y2 in P and

         A2: ( dist (y1,y2)) = ( min_dist_min (Q,P)) by WEIERSTR: 30;

        consider x1,x2 be Point of M such that

         A3: x1 in P & x2 in Q and

         A4: ( dist (x1,x2)) = ( min_dist_min (P,Q)) by WEIERSTR: 30;

        ( dist (x1,x2)) <= ( dist (y1,y2)) & ( dist (y1,y2)) <= ( dist (x1,x2)) by A1, A2, A3, A4, WEIERSTR: 34;

        hence thesis by A2, A4, XXREAL_0: 1;

      end;

      :: original: max_dist_max

      redefine

      func max_dist_max (P,Q);

      commutativity

      proof

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

        consider y1,y2 be Point of M such that

         A5: y1 in Q & y2 in P and

         A6: ( dist (y1,y2)) = ( max_dist_max (Q,P)) by WEIERSTR: 33;

        consider x1,x2 be Point of M such that

         A7: x1 in P & x2 in Q and

         A8: ( dist (x1,x2)) = ( max_dist_max (P,Q)) by WEIERSTR: 33;

        ( dist (x1,x2)) <= ( dist (y1,y2)) & ( dist (y1,y2)) <= ( dist (x1,x2)) by A5, A6, A7, A8, WEIERSTR: 34;

        hence thesis by A6, A8, XXREAL_0: 1;

      end;

    end

    definition

      let n;

      let A,B be non empty compact Subset of ( TOP-REAL n);

      :: original: dist_min

      redefine

      func dist_min (A,B);

      commutativity

      proof

        let A,B be non empty compact Subset of ( TOP-REAL n);

        consider A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) such that

         A1: A = A9 & B = B9 and

         A2: ( dist_min (A,B)) = ( min_dist_min (A9,B9)) by Def1;

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider A9, B9 as non empty compact Subset of ( TopSpaceMetr ( Euclid n)) by A1, COMPTS_1: 23;

        ( dist_min (A,B)) = ( min_dist_min (B9,A9)) by A2;

        hence thesis by A1, Def1;

      end;

    end

    theorem :: JORDAN1K:38

    

     Th38: for A,B be non empty Subset of ( TOP-REAL n) holds ( dist_min (A,B)) >= 0

    proof

      let A,B be non empty Subset of ( TOP-REAL n);

      ex A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) st A = A9 & B = B9 & ( dist_min (A,B)) = ( min_dist_min (A9,B9)) by Def1;

      hence thesis by Th11;

    end;

    theorem :: JORDAN1K:39

    

     Th39: for A,B be compact Subset of ( TOP-REAL n) st A meets B holds ( dist_min (A,B)) = 0

    proof

      let A,B be compact Subset of ( TOP-REAL n) such that

       A1: A meets B;

      consider A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) such that

       A2: A = A9 & B = B9 and

       A3: ( dist_min (A,B)) = ( min_dist_min (A9,B9)) by Def1;

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then A9 is compact & B9 is compact by A2, COMPTS_1: 23;

      hence thesis by A1, A2, A3, Th12;

    end;

    theorem :: JORDAN1K:40

    

     Th40: for A,B be non empty Subset of ( TOP-REAL n) st for p,q be Point of ( TOP-REAL n) st p in A & q in B holds ( dist (p,q)) >= r holds ( dist_min (A,B)) >= r

    proof

      let A,B be non empty Subset of ( TOP-REAL n) such that

       A1: for p,q be Point of ( TOP-REAL n) st p in A & q in B holds ( dist (p,q)) >= r;

      

       A2: for p,q be Point of ( Euclid n) st p in A & q in B holds ( dist (p,q)) >= r

      proof

        let a,b be Point of ( Euclid n) such that

         A3: a in A & b in B;

        reconsider p = a, q = b as Point of ( TOP-REAL n) by TOPREAL3: 8;

        ex a,b be Point of ( Euclid n) st p = a & q = b & ( dist (p,q)) = ( dist (a,b)) by TOPREAL6:def 1;

        hence thesis by A1, A3;

      end;

      ex A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) st A = A9 & B = B9 & ( dist_min (A,B)) = ( min_dist_min (A9,B9)) by Def1;

      hence thesis by A2, Th13;

    end;

    theorem :: JORDAN1K:41

    

     Th41: for D be Subset of ( TOP-REAL n), A,C be non empty Subset of ( TOP-REAL n) st C c= D holds ( dist_min (A,D)) <= ( dist_min (A,C))

    proof

      let D be Subset of ( TOP-REAL n);

      let A,C be non empty Subset of ( TOP-REAL n) such that

       A1: C c= D;

      consider A9,D9 be Subset of ( TopSpaceMetr ( Euclid n)) such that

       A2: A = A9 and

       A3: D = D9 & ( dist_min (A,D)) = ( min_dist_min (A9,D9)) by Def1;

      reconsider f = ( dist_min A9) as Function of the carrier of ( TopSpaceMetr ( Euclid n)), REAL by TOPMETR: 17;

      reconsider Y = (f .: D9) as Subset of REAL ;

      

       A4: Y is bounded_below

      proof

        take 0 ;

        let r be ExtReal;

        assume r in Y;

        then ex c be Element of ( TopSpaceMetr ( Euclid n)) st c in D9 & r = (f . c) by FUNCT_2: 65;

        hence thesis by A2, Th9;

      end;

      

       A5: ( lower_bound Y) = ( lower_bound ( [#] (( dist_min A9) .: D9))) by WEIERSTR:def 1

      .= ( lower_bound (( dist_min A9) .: D9)) by WEIERSTR:def 3

      .= ( min_dist_min (A9,D9)) by WEIERSTR:def 7;

      consider A99,C9 be Subset of ( TopSpaceMetr ( Euclid n)) such that

       A6: A = A99 and

       A7: C = C9 and

       A8: ( dist_min (A,C)) = ( min_dist_min (A99,C9)) by Def1;

      ( dom f) = the carrier of ( TopSpaceMetr ( Euclid n)) by FUNCT_2:def 1;

      then

      reconsider X = (f .: C9) as non empty Subset of REAL by A7;

      ( lower_bound X) = ( lower_bound ( [#] (( dist_min A9) .: C9))) by WEIERSTR:def 1

      .= ( lower_bound (( dist_min A9) .: C9)) by WEIERSTR:def 3

      .= ( min_dist_min (A9,C9)) by WEIERSTR:def 7;

      hence thesis by A1, A2, A3, A6, A7, A8, A5, A4, RELAT_1: 123, SEQ_4: 47;

    end;

    theorem :: JORDAN1K:42

    

     Th42: for A,B be non empty compact Subset of ( TOP-REAL n) holds ex p,q be Point of ( TOP-REAL n) st p in A & q in B & ( dist_min (A,B)) = ( dist (p,q))

    proof

      let A,B be non empty compact Subset of ( TOP-REAL n);

      consider A9,B9 be Subset of ( TopSpaceMetr ( Euclid n)) such that

       A1: A = A9 & B = B9 and

       A2: ( dist_min (A,B)) = ( min_dist_min (A9,B9)) by Def1;

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then A9 is compact & B9 is compact by A1, COMPTS_1: 23;

      then

      consider x1,x2 be Point of ( Euclid n) such that

       A3: x1 in A9 & x2 in B9 and

       A4: ( dist (x1,x2)) = ( min_dist_min (A9,B9)) by A1, WEIERSTR: 30;

      reconsider p = x1, q = x2 as Point of ( TOP-REAL n) by TOPREAL3: 8;

      take p, q;

      thus p in A & q in B by A1, A3;

      thus thesis by A2, A4, TOPREAL6:def 1;

    end;

    theorem :: JORDAN1K:43

    

     Th43: for p,q be Point of ( TOP-REAL n) holds ( dist_min ( {p}, {q})) = ( dist (p,q))

    proof

      let p,q be Point of ( TOP-REAL n);

      consider p9,q9 be Point of ( TOP-REAL n) such that

       A1: p9 in {p} and

       A2: q9 in {q} & ( dist_min ( {p}, {q})) = ( dist (p9,q9)) by Th42;

      p = p9 by A1, TARSKI:def 1;

      hence thesis by A2, TARSKI:def 1;

    end;

    definition

      let n;

      let p be Point of ( TOP-REAL n);

      let B be Subset of ( TOP-REAL n);

      :: JORDAN1K:def2

      func dist (p,B) -> Real equals ( dist_min ( {p},B));

      coherence ;

    end

    theorem :: JORDAN1K:44

    for A be non empty Subset of ( TOP-REAL n), p be Point of ( TOP-REAL n) holds ( dist (p,A)) >= 0 by Th38;

    theorem :: JORDAN1K:45

    for A be compact Subset of ( TOP-REAL n), p be Point of ( TOP-REAL n) st p in A holds ( dist (p,A)) = 0 by Th39, ZFMISC_1: 48;

    theorem :: JORDAN1K:46

    

     Th46: for A be non empty compact Subset of ( TOP-REAL n), p be Point of ( TOP-REAL n) holds ex q be Point of ( TOP-REAL n) st q in A & ( dist (p,A)) = ( dist (p,q))

    proof

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

      let p be Point of ( TOP-REAL n);

      consider q,p9 be Point of ( TOP-REAL n) such that

       A1: q in A and

       A2: p9 in {p} & ( dist_min (A, {p})) = ( dist (q,p9)) by Th42;

      take q;

      thus q in A by A1;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: JORDAN1K:47

    for C be non empty Subset of ( TOP-REAL n) holds for D be Subset of ( TOP-REAL n) st C c= D holds for q be Point of ( TOP-REAL n) holds ( dist (q,D)) <= ( dist (q,C)) by Th41;

    theorem :: JORDAN1K:48

    for A be non empty Subset of ( TOP-REAL n), p be Point of ( TOP-REAL n) st for q be Point of ( TOP-REAL n) st q in A holds ( dist (p,q)) >= r holds ( dist (p,A)) >= r

    proof

      let A be non empty Subset of ( TOP-REAL n), p9 be Point of ( TOP-REAL n) such that

       A1: for q be Point of ( TOP-REAL n) st q in A holds ( dist (p9,q)) >= r;

      for p,q be Point of ( TOP-REAL n) st p in {p9} & q in A holds ( dist (p,q)) >= r

      proof

        let p,q be Point of ( TOP-REAL n) such that

         A2: p in {p9} and

         A3: q in A;

        p = p9 by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      hence thesis by Th40;

    end;

    theorem :: JORDAN1K:49

    for p,q be Point of ( TOP-REAL n) holds ( dist (p, {q})) = ( dist (p,q)) by Th43;

    theorem :: JORDAN1K:50

    

     Th50: for A be non empty Subset of ( TOP-REAL n), p,q be Point of ( TOP-REAL n) st q in A holds ( dist (p,A)) <= ( dist (p,q))

    proof

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

      let p,q be Point of ( TOP-REAL n);

      assume q in A;

      then {q} c= A by ZFMISC_1: 31;

      then ( dist (p,A)) <= ( dist (p, {q})) by Th41;

      hence thesis by Th43;

    end;

    theorem :: JORDAN1K:51

    for A be compact non empty Subset of ( TOP-REAL 2), B be open Subset of ( TOP-REAL 2) st A c= B holds for p be Point of ( TOP-REAL 2) st not p in B holds ( dist (p,B)) < ( dist (p,A))

    proof

      let A be compact non empty Subset of ( TOP-REAL 2), B be open Subset of ( TOP-REAL 2) such that

       A1: A c= B;

       the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

      then

      reconsider P = B as open Subset of ( TopSpaceMetr ( Euclid 2)) by PRE_TOPC: 30;

      let p be Point of ( TOP-REAL 2) such that

       A2: not p in B;

      assume

       A3: ( dist (p,B)) >= ( dist (p,A));

      ( dist (p,B)) <= ( dist (p,A)) by A1, Th41;

      then

       A4: ( dist (p,B)) = ( dist (p,A)) by A3, XXREAL_0: 1;

      consider q be Point of ( TOP-REAL 2) such that

       A5: q in A and

       A6: ( dist (p,A)) = ( dist (p,q)) by Th46;

      reconsider a = q as Point of ( Euclid 2) by TOPREAL3: 8;

      consider r be Real such that

       A7: r > 0 and

       A8: ( Ball (a,r)) c= P by A1, A5, TOPMETR: 15;

      reconsider r as Element of REAL by XREAL_0:def 1;

      set s = (r / (2 * ( dist (p,q)))), q9 = (((1 - s) * q) + (s * p));

      a in P by A1, A5;

      then

       A9: ( dist (p,q)) > 0 by A2, Th22;

      then

       A10: (2 * ( dist (p,q))) > 0 by XREAL_1: 129;

      then 0 < s by A7, XREAL_1: 139;

      then

       A11: (1 - s) < (1 - 0 ) by XREAL_1: 10;

      

       A12: ex p1,q1 be Point of ( Euclid 2) st p1 = q & q1 = q9 & ( dist (q,q9)) = ( dist (p1,q1)) by TOPREAL6:def 1;

      ( dist (q,q9)) = (((1 * r) / (2 * ( dist (p,q)))) * ( dist (p,q))) by A7, A9, Th28

      .= (((r / 2) / (( dist (p,q)) / 1)) * ( dist (p,q))) by XCMPLX_1: 84

      .= (r / 2) by A9, XCMPLX_1: 87;

      then ( dist (q,q9)) < (r / 1) by A7, XREAL_1: 76;

      then

       A13: q9 in ( Ball (a,r)) by A12, METRIC_1: 11;

      now

        

         A14: ex p1,q1 be Point of ( Euclid 2) st p1 = p & q1 = q & ( dist (p,q)) = ( dist (p1,q1)) by TOPREAL6:def 1;

        assume r > ( dist (p,q));

        then p in ( Ball (a,r)) by A14, METRIC_1: 11;

        hence contradiction by A2, A8;

      end;

      then (1 * r) < (2 * ( dist (p,q))) by A7, XREAL_1: 98;

      then s < 1 by A10, XREAL_1: 191;

      then ( dist (p,q9)) = ((1 - s) * ( dist (p,q))) by Th27;

      hence contradiction by A4, A6, A8, A9, A13, A11, Th50, XREAL_1: 157;

    end;