JORDAN1K

:: On the Minimal Distance Between Set in {E}uclidean Space
::  by Andrzej Trybulec
::
:: Received August 19, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, FUNCT_1, FUNCT_2, SUBSET_1, RELAT_1, TARSKI,
      PRE_TOPC, CONNSP_1, RELAT_2, XXREAL_0, EUCLID, XXREAL_2, STRUCT_0,
      REAL_1, METRIC_1, PCOMPS_1, WEIERSTR, CARD_1, SEQ_4, RCOMP_1, JORDAN2C,
      COMPLEX1, SQUARE_1, MCART_1, ARYTM_1, ARYTM_3, RLTOPSP1, JGRAPH_2, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
      XREAL_0, COMPLEX1, REAL_1, SQUARE_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, XXREAL_2, SEQ_4, DOMAIN_1, STRUCT_0, PRE_TOPC, COMPTS_1,
      CONNSP_1, METRIC_1, METRIC_6, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID,
      WEIERSTR, JORDAN2C, TOPREAL6, JGRAPH_2;
 constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, CONNSP_1, COMPTS_1, TBSP_1,
      MONOID_0, WEIERSTR, JORDAN2C, TOPREAL6, JGRAPH_2, FUNCSDOM, BINOP_2,
      CONVEX1;
 registrations XBOOLE_0, FUNCT_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0,
      MEMBERED, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, PCOMPS_1, MONOID_0,
      EUCLID, TOPMETR, JORDAN2C, BORSUK_3, TOPREAL6, JGRAPH_2, RELSET_1,
      JORDAN1, VALUED_0, JORDAN5A, SQUARE_1, ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions XBOOLE_0, TARSKI, FUNCT_2, XXREAL_2;
 equalities EUCLID, SQUARE_1, SUBSET_1, STRUCT_0, RLTOPSP1, RLVECT_1;
 expansions XBOOLE_0, TARSKI, FUNCT_2;
 theorems XBOOLE_1, XBOOLE_0, SPRECT_1, JORDAN2C, SUBSET_1, GOBOARD9, TSEP_1,
      CONNSP_1, PRE_TOPC, ZFMISC_1, EUCLID, WEIERSTR, TOPREAL3, TBSP_1,
      SQUARE_1, ABSVALUE, FUNCT_1, METRIC_1, FUNCT_2, JGRAPH_2, RELAT_1,
      TOPMETR, PCOMPS_1, TARSKI, XREAL_0, TOPRNS_1, XCMPLX_1, COMPLEX1, SEQ_4,
      XREAL_1, XXREAL_0, TOPS_2, TOPREAL6, COMPTS_1, RLVECT_1;

begin :: Preliminaries

reserve X for set,
  Y for non empty set;

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

theorem
  for f being Function of X,Y st f is onto for y being Element of Y ex x
  being 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 being object st x in X & f.x = y by A1,Th1;
  hence thesis;
end;

theorem Th3:
  for f being Function of X,Y, A being 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 being 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 Th4:
  for f being Function of X,Y, A being 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 being 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 being 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 Th5:
  for f being Function of X,Y, A being Subset of X st f is
  bijective holds (f.:A)` = f.:A`
by Th3,Th4;

begin :: Topological and metrizable spaces

theorem Th6:
  for T being TopSpace 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 being 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 Th7:
  for T being non empty TopSpace for A,B,C being 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
  n >= 1 implies for P being Subset of Euclid n holds P is bounded
  implies P` is not 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 Th9:
  for C being non empty Subset of TopSpaceMetr M, p being 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 being Real st r in B holds 0 <= r
  proof
    let r be Real;
    assume r in B;
    then consider y being 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 Th10:
  for C being non empty Subset of TopSpaceMetr M, p being Point of
M st for q being 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 being 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 being Real st s in B holds r <= s
  proof
    let s be Real;
    assume s in B;
    then consider y being 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 Th11:
  for A,B being 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 being Real st r in X holds 0 <= r
  proof
    let r be Real;
    assume r in X;
    then consider y being 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 Th12:
  for A,B being 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 being 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 Th13:
  for A,B being non empty Subset of TopSpaceMetr M st for p,q
being 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 being 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 being Real st s in X holds r <= s
  proof
    let s be Real;
    assume s in X;
    then consider y being 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 being 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 :: Euclid topological spaces

theorem Th14:
  for P,Q being 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,def 3;

theorem
  n>= 1 implies BDD {}TOP-REAL n = {}TOP-REAL n
proof
  set X = {B where B is Subset of TOP-REAL n: B is_inside_component_of {}(
  TOP-REAL n)};
  assume n>= 1;
  then
A1: [#](TOP-REAL n) is not 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 being object such that
A4: x in X by XBOOLE_0:def 1;
    consider B being 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
  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
  n>= 1 implies UBD {}TOP-REAL n = [#]TOP-REAL n
proof
  set X = {B where B is Subset of TOP-REAL n: B is_outside_component_of {}
  TOP-REAL n};
  assume n>= 1;
  then
A1: [#](TOP-REAL n) is not 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
  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
  for P being connected Subset of TOP-REAL n, Q being 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 being 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: P is not empty and
 Q <> [#]TOP-REAL n;
    P c= Q` by A1,SUBSET_1:23;
    then consider C being 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,23;
    hence thesis by A4;
  end;
end;

begin :: Euclid plane

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 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 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 Th22:
  p <> q implies dist(p,q) > 0
proof
  ex p9, q9 being 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 Th23:
  dist(q1-q,q2-q) = dist(q1,q2) by Th21;

theorem 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 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 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 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 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 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
  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 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 :: Affine maps

theorem 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 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 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 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 being 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 being 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 being 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 being 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 Th36:
  for A,B,C,D being 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
  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 :: Minimal distance between subsets

definition
  let n;
  let A,B be Subset of TOP-REAL n;
  func dist_min(A,B) -> Real means
  :Def1:
  ex A9,B9 being 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;
  redefine func min_dist_min(P,Q);  :: redefines min_dist_min (WEIERSTR, definition)
  commutativity
  proof
    let P,Q be non empty compact Subset of TopSpaceMetr M;
    consider y1,y2 being 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 being 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;
  redefine func max_dist_max(P,Q);  :: redefines max_dist_max (WEIERSTR, definition)
  commutativity
  proof
    let P,Q be non empty compact Subset of TopSpaceMetr M;
    consider y1,y2 being 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 being 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;
  redefine func dist_min(A,B);  :: redefines dist_min (JORDAN1K, definition)
  commutativity
  proof
    let A,B be non empty compact Subset of TOP-REAL n;
    consider A9,B9 being 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 Th38:
  for A,B being 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 Th39:
  for A,B being 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 Th40:
  for A,B being non empty Subset of TOP-REAL n st for p,q being
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 being Point of TOP-REAL n st p in A & q in B holds dist(p,q) >= r;
A2: for p,q being Point of Euclid n st p in A & q in B holds dist(p,q) >= r
  proof
    let a,b being 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 being 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 Th41:
  for D being Subset of TOP-REAL n, A,C being 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 being 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 Th42:
  for A,B being non empty compact Subset of TOP-REAL n ex p,q
  being 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 being 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 being 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 Th43:
  for p,q being 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 being 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;
  func dist(p,B) -> Real equals
  dist_min({p},B);
  coherence;
end;

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

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

theorem Th46:
  for A being non empty compact Subset of TOP-REAL n, p being
Point of TOP-REAL n ex q being 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 being 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
  for C being non empty Subset of TOP-REAL n for D being Subset of
TOP-REAL n st C c= D for q being Point of TOP-REAL n holds dist(q,D) <= dist(q,
  C) by Th41;

theorem
  for A being non empty Subset of TOP-REAL n, p being Point of TOP-REAL
n st for q being 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 being Point of TOP-REAL n st q in A holds dist(p9,q) >= r;
  for p,q being 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
  for p,q being Point of TOP-REAL n holds dist(p,{q}) = dist(p,q) by Th43;

theorem Th50:
  for A being non empty Subset of TOP-REAL n, p,q being 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
  for A being compact non empty Subset of TOP-REAL 2, B being open
  Subset of TOP-REAL 2 st A c= B for p being 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 being 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 being 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 being 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 being 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 being 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;