:: On the Minimal Distance Between Set in {E}uclidean Space
::  by Andrzej Trybulec
::
:: Received August 19, 2002
:: Copyright (c) 2002-2021 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;


begin :: Preliminaries

reserve X for set,
  Y for non empty set;

theorem :: JORDAN1K:1
  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;

theorem :: JORDAN1K:2
  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;

theorem :: JORDAN1K:3
  for f being Function of X,Y, A being Subset of X st f is onto
  holds (f.:A)` c= f.:A`;

theorem :: JORDAN1K:4
  for f being Function of X,Y, A being Subset of X st f is
  one-to-one holds f.:A` c= (f.:A)`;

theorem :: JORDAN1K:5
  for f being Function of X,Y, A being Subset of X st f is
  bijective holds (f.:A)` = f.:A`;

begin :: Topological and metrizable spaces

theorem :: JORDAN1K:6
  for T being TopSpace for A be Subset of T holds A
  is_a_component_of {}T iff A is empty;

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

reserve n for Nat;

theorem :: JORDAN1K:8
  n >= 1 implies for P being Subset of Euclid n holds P is bounded
  implies P` is not bounded;

reserve r for Real,
  M for non empty MetrSpace;

theorem :: JORDAN1K:9
  for C being non empty Subset of TopSpaceMetr M, p being Point of
  TopSpaceMetr M holds (dist_min C).p >= 0;

theorem :: JORDAN1K:10
  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;

theorem :: JORDAN1K:11
  for A,B being non empty Subset of TopSpaceMetr M holds min_dist_min(A,B) >= 0
;

theorem :: JORDAN1K:12
  for A,B being compact Subset of TopSpaceMetr M st A meets B
  holds min_dist_min(A,B) = 0;

theorem :: JORDAN1K:13
  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;

begin :: Euclid topological spaces

theorem :: JORDAN1K:14
  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;

theorem :: JORDAN1K:15
  n>= 1 implies BDD {}TOP-REAL n = {}TOP-REAL n;

theorem :: JORDAN1K:16
  BDD [#]TOP-REAL n = {}TOP-REAL n;

theorem :: JORDAN1K:17
  n>= 1 implies UBD {}TOP-REAL n = [#]TOP-REAL n;

theorem :: JORDAN1K:18
  UBD [#]TOP-REAL n = {}TOP-REAL n;

theorem :: JORDAN1K:19
  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;

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 :: JORDAN1K:20
  dist(|[0,0]|,r*q) = |.r.|*dist(|[0,0]|,q);

theorem :: JORDAN1K:21
  dist(q1+q,q2+q) = dist(q1,q2);

theorem :: JORDAN1K:22
  p <> q implies dist(p,q) > 0;

theorem :: JORDAN1K:23
  dist(q1-q,q2-q) = dist(q1,q2);

theorem :: JORDAN1K:24
  dist(p,q) = dist(-p,-q);

theorem :: JORDAN1K:25
  dist(q-q1,q-q2) = dist(q1,q2);

theorem :: JORDAN1K:26
  dist(r*p,r*q) = |.r.|*dist(p,q);

theorem :: JORDAN1K:27
  r <= 1 implies dist(p,r*p+(1-r)*q) = (1-r)*dist(p,q);

theorem :: JORDAN1K:28
  0 <= r implies dist(q,r*p+(1-r)*q) = r*dist(p,q);

theorem :: JORDAN1K:29
  p in LSeg(q1,q2) implies dist(q1,p) + dist(p,q2) = dist(q1,q2);

theorem :: JORDAN1K:30
  q1 in LSeg(q2,p) & q1 <> q2 implies dist(q1,p) < dist(q2,p);

theorem :: JORDAN1K:31
  y = |[0,0]| implies Ball(y,r) = {q : |.q.| < r };

begin :: Affine maps

theorem :: JORDAN1K:32
  AffineMap(r,s1,r,s2).p = r*p+|[s1,s2]|;

theorem :: JORDAN1K:33
  AffineMap(r,q`1,r,q`2).p = r*p+q;

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

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

theorem :: JORDAN1K:36
  for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C,D) is onto;

theorem :: JORDAN1K:37
  Ball(x,r)` is connected Subset of TOP-REAL 2;

begin :: Minimal distance between subsets

definition
  let n;
  let A,B be Subset of TOP-REAL n;
  func dist_min(A,B) -> Real means
:: JORDAN1K:def 1

  ex A9,B9 being Subset of
  TopSpaceMetr Euclid n st A = A9 & B = B9 & it = min_dist_min(A9,B9);
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);
  commutativity;
  redefine func max_dist_max(P,Q);
  commutativity;
end;

definition
  let n;
  let A,B be non empty compact Subset of TOP-REAL n;
  redefine func dist_min(A,B);
  commutativity;
end;

theorem :: JORDAN1K:38
  for A,B being non empty Subset of TOP-REAL n holds dist_min(A,B) >= 0;

theorem :: JORDAN1K:39
  for A,B being compact Subset of TOP-REAL n st A meets B holds
  dist_min(A,B) = 0;

theorem :: JORDAN1K:40
  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;

theorem :: JORDAN1K:41
  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);

theorem :: JORDAN1K:42
  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);

theorem :: JORDAN1K:43
  for p,q being Point of TOP-REAL n holds dist_min({p},{q}) = dist (p,q);

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
:: JORDAN1K:def 2
  dist_min({p},B);
end;

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

theorem :: JORDAN1K:45
  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;

theorem :: JORDAN1K:46
  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);

theorem :: JORDAN1K:47
  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);

theorem :: JORDAN1K:48
  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;

theorem :: JORDAN1K:49
  for p,q being Point of TOP-REAL n holds dist(p,{q}) = dist(p,q);

theorem :: JORDAN1K:50
  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);

theorem :: JORDAN1K:51
  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);