:: Metric Spaces
::  by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek
::
:: Received May 3, 1990
:: Copyright (c) 1990-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, STRUCT_0, FUNCT_1, ZFMISC_1, XBOOLE_0, PARTFUN1,
      SUBSET_1, REAL_1, RELAT_1, CARD_1, FUNCT_5, TARSKI, VALUED_0, ORDINAL1,
      XXREAL_0, ARYTM_3, RELAT_2, FUNCT_3, COMPLEX1, ARYTM_1, METRIC_1,
      FUNCOP_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCOP_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_5, VALUED_0,
      STRUCT_0;
 constructors BINOP_1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, STRUCT_0, VALUED_1,
      FUNCT_5, PARTFUN1, RELSET_1, FUNCOP_1, NUMBERS;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, MEMBERED,
      STRUCT_0, VALUED_0, FUNCT_2, PARTFUN1, RELSET_1, ORDINAL1, BINOP_2;
 requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;


begin

definition
  struct(1-sorted) MetrStruct
   (# carrier -> set,
     distance -> Function of [:the carrier,the carrier:],REAL #);
end;

registration
  cluster non empty strict for MetrStruct;
end;

:: registration
::   let A,B be set, f be PartFunc of [:A,B:],REAL;
::   let a be Element of A;
::   let b be Element of B;
::   cluster f.(a,b) -> real;
::   coherence
::   proof
::     per cases;
::     suppose
::       [a,b] in dom f;
::       hence thesis by PARTFUN1:4;
::     end;
::     suppose
::       not [a,b] in dom f;
::       then f.(a,b) = 0 by FUNCT_1:def 2;
::       hence thesis;
::     end;
::   end;
:: end;

definition
  let M be MetrStruct;
  let a, b be Element of M;
  func dist(a,b) -> Real equals
:: METRIC_1:def 1
  (the distance of M).(a,b);
end;

notation
  synonym Empty^2-to-zero for op2;
end;

definition
  redefine func Empty^2-to-zero -> Function of [:1,1:], REAL;
end;

registration
  cluster op2 -> natural-valued for Function;
end;

registration
  let f be natural-valued Function;
  let x,y be object;
  cluster f.(x,y) -> natural;
end;

definition

  let A be set;
  let f be PartFunc of [:A,A:], REAL;
  attr f is Reflexive means
:: METRIC_1:def 2

  for a being Element of A holds f.(a,a) = 0;
  attr f is discerning means
:: METRIC_1:def 3

  for a, b being Element of A st f.(a,b) = 0 holds a = b;
  attr f is symmetric means
:: METRIC_1:def 4

  for a, b being Element of A holds f.(a,b) = f.(b,a);
  attr f is triangle means
:: METRIC_1:def 5

  for a, b, c being Element of A holds f.(a,c) <= f.(a,b) + f.(b,c);
end;

definition
  let M be MetrStruct;
  attr M is Reflexive means
:: METRIC_1:def 6

  the distance of M is Reflexive;
  attr M is discerning means
:: METRIC_1:def 7

  the distance of M is discerning;
  attr M is symmetric means
:: METRIC_1:def 8

  the distance of M is symmetric;
  attr M is triangle means
:: METRIC_1:def 9

  the distance of M is triangle;
end;

registration
  cluster strict Reflexive discerning symmetric triangle non empty for
MetrStruct;
end;

definition
  mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct;
end;

theorem :: METRIC_1:1
  for M being MetrStruct holds ( for a being Element of M holds
  dist(a,a) = 0 ) iff M is Reflexive;

theorem :: METRIC_1:2
  for M being MetrStruct holds
  ( for a, b being Element of M st dist(a,b) = 0 holds a = b ) iff
  M is discerning;

theorem :: METRIC_1:3
  for M being MetrStruct st
   for a, b being Element of M holds dist(a,b) = dist(b,a) holds
  M is symmetric;

theorem :: METRIC_1:4
  for M being MetrStruct holds ( for a, b, c being Element of M
  holds dist(a,c) <= dist(a,b) + dist(b,c) ) iff M is triangle;

definition
  let M be symmetric MetrStruct;
  let a, b be Element of M;
  redefine func dist(a,b);
  commutativity;
end;

theorem :: METRIC_1:5
  for M being symmetric triangle Reflexive MetrStruct,
      a, b being Element of M holds 0 <= dist(a,b);

theorem :: METRIC_1:6
  for M being MetrStruct st (for a, b, c being Element of M holds
  (dist(a,b) = 0 iff a=b) &
  dist(a,b) = dist(b,a) &
  dist(a,c) <= dist(a,b) + dist(b,c)) holds M is MetrSpace;

theorem :: METRIC_1:7
  for M being MetrSpace, x,y being Element of M st x <> y holds 0 < dist(x,y);

definition
  let A be set;
  func discrete_dist A -> Function of [:A,A:], REAL means
:: METRIC_1:def 10

  for x,y being Element of A holds it.(x,x) = 0 &
  (x <> y implies it.(x,y) = 1);
end;

definition
  let A be set;
  func DiscreteSpace A -> strict MetrStruct equals
:: METRIC_1:def 11
  MetrStruct (#A,discrete_dist A#);
end;

registration
  let A be non empty set;
  cluster DiscreteSpace A -> non empty;
end;

registration
  let A be set;
  cluster DiscreteSpace A -> Reflexive discerning symmetric triangle;
end;

definition
  func real_dist -> Function of [:REAL,REAL:], REAL means
:: METRIC_1:def 12

  for x,y being Real holds it.(x,y) = |.x-y.|;
end;

theorem :: METRIC_1:8
  for x,y being Element of REAL holds real_dist.(x,y) = 0 iff x = y;

theorem :: METRIC_1:9
  for x,y being Element of REAL holds real_dist.(x,y) = real_dist.(y,x);

theorem :: METRIC_1:10
  for x,y,z being Element of REAL holds real_dist.(x,y) <=
  real_dist.(x,z) + real_dist.(z,y);

definition
  func RealSpace -> strict MetrStruct equals
:: METRIC_1:def 13
  MetrStruct (# REAL, real_dist #);
end;

registration
  cluster RealSpace -> non empty;
end;

registration
  cluster RealSpace -> Reflexive discerning symmetric triangle;
end;

definition
  let M be MetrStruct, p be Element of M, r be Real;
  func Ball(p,r) -> Subset of M means
:: METRIC_1:def 14

   it = {q where q is Element of M : dist(p,q) < r} if M is non empty
    otherwise it is empty;
end;

definition
  let M be MetrStruct, p be Element of M, r be Real;
  func cl_Ball(p,r) -> Subset of M means
:: METRIC_1:def 15

     it = {q where q is Element of M : dist(p,q) <= r} if M is non empty
      otherwise it is empty;
end;

definition
  let M be MetrStruct, p be Element of M, r be Real;
  func Sphere(p,r) -> Subset of M means
:: METRIC_1:def 16

   it = {q where q is Element of M : dist(p,q) = r} if M is non empty
   otherwise it is empty;
end;

reserve r for Real;

theorem :: METRIC_1:11
  for M being MetrStruct, p, x being Element of M holds x in Ball(p,r)
    iff M is non empty & dist(p,x) < r;

theorem :: METRIC_1:12
  for M being MetrStruct, p, x being Element of M holds x in
  cl_Ball(p,r) iff M is non empty & dist(p,x) <= r;

theorem :: METRIC_1:13
  for M being MetrStruct, p, x being Element of M holds x in
  Sphere(p,r) iff M is non empty & dist(p,x) = r;

theorem :: METRIC_1:14
  for M being MetrStruct, p being Element of M holds Ball(p,r) c= cl_Ball(p,r);

theorem :: METRIC_1:15
  for M being MetrStruct, p being Element of M holds Sphere(p,r)
  c= cl_Ball(p,r);

theorem :: METRIC_1:16
  for M being MetrStruct, p being Element of M holds
  Sphere(p,r) \/ Ball(p,r) = cl_Ball(p,r);

theorem :: METRIC_1:17
  for M being non empty MetrStruct, p being Element of M holds Ball(p,r)
  = {q where q is Element of M: dist(p,q) < r};

theorem :: METRIC_1:18
  for M being non empty MetrStruct, p being Element of M holds cl_Ball(p
  ,r) = {q where q is Element of M: dist(p,q) <= r};

theorem :: METRIC_1:19
  for M being non empty MetrStruct, p being Element of M holds Sphere(p,
  r) = {q where q is Element of M: dist(p,q) = r};

begin :: SUB_METR

theorem :: METRIC_1:20
  for x being set holds Empty^2-to-zero.(x,x) = 0;

theorem :: METRIC_1:21
  for x,y being Element of 1 st x <> y holds 0 < Empty^2-to-zero.(x,y);

theorem :: METRIC_1:22
  for x,y being Element of 1 holds
    Empty^2-to-zero.(x,y) = Empty^2-to-zero.(y,x);

theorem :: METRIC_1:23
  for x,y,z being Element of 1 holds Empty^2-to-zero.(x,z) <=
  Empty^2-to-zero.(x,y) + Empty^2-to-zero.(y,z);

theorem :: METRIC_1:24
  for x,y,z being Element of 1 holds
  Empty^2-to-zero.(x,z) <= max(Empty^2-to-zero.(x,y),Empty^2-to-zero.(y,z));

definition
  let A be non empty set;
  let f be Function of [:A,A:], REAL;
  attr f is Discerning means
:: METRIC_1:def 17

  for a, b being Element of A holds a <> b implies 0 < f.(a,b);
end;

definition
  let M be non empty MetrStruct;
  attr M is Discerning means
:: METRIC_1:def 18

  the distance of M is Discerning;
end;

theorem :: METRIC_1:25
  for M being non empty MetrStruct holds
  ( for a, b being Element of M holds a <> b implies 0 < dist(a,b)) iff
  M is Discerning;

registration
  cluster MetrStruct(#1,Empty^2-to-zero#) -> non empty;
end;

registration
  cluster MetrStruct(#1,Empty^2-to-zero#) -> Reflexive symmetric Discerning
    triangle;
end;

definition
  let M be non empty MetrStruct;
  attr M is ultra means
:: METRIC_1:def 19
  for a, b, c being Element of M holds dist(a,c) <= max (dist(a,b),dist(b,c));
end;

registration
  cluster strict ultra Reflexive symmetric Discerning triangle
    for non empty MetrStruct;
end;

theorem :: METRIC_1:26
  for M being Reflexive Discerning non empty MetrStruct,
      a,b being Element of M holds 0 <= dist(a,b);

definition
  mode PseudoMetricSpace is Reflexive symmetric triangle
    non empty MetrStruct;
  mode SemiMetricSpace is Reflexive Discerning symmetric
    non empty MetrStruct;
  mode NonSymmetricMetricSpace is Reflexive Discerning triangle
    non empty MetrStruct;
  mode UltraMetricSpace is ultra Reflexive symmetric Discerning
    non empty MetrStruct;
end;

registration
  cluster -> Discerning for non empty MetrSpace;
end;

registration
  cluster -> triangle discerning for UltraMetricSpace;
end;

definition
  func Set_to_zero -> Function of [:2,2:],REAL equals
:: METRIC_1:def 20
  [:2,2:] --> 0;
end;

theorem :: METRIC_1:27
  for x,y being Element of 2 holds Set_to_zero.(x,y) = 0;

theorem :: METRIC_1:28
  for x,y being Element of 2 holds Set_to_zero.(x,y) = Set_to_zero.(y,x);

theorem :: METRIC_1:29
  for x,y,z being Element of 2 holds
  Set_to_zero.(x,z) <= Set_to_zero.(x,y) + Set_to_zero.(y,z);

definition
  func ZeroSpace -> MetrStruct equals
:: METRIC_1:def 21
  MetrStruct(#2, Set_to_zero#);
end;

registration
  cluster ZeroSpace -> strict non empty;
end;

registration
  cluster ZeroSpace -> Reflexive symmetric triangle;
end;

definition
  let S be MetrStruct, p,q,r be Element of S;
  pred q is_between p,r means
:: METRIC_1:def 22
  p <> q & p <> r & q <> r & dist(p,r) = dist(p,q) + dist(q,r);
end;

theorem :: METRIC_1:30
  for S being symmetric triangle Reflexive non empty MetrStruct,
      p, q, r being Element of S holds
    q is_between p,r implies q is_between r,p;

theorem :: METRIC_1:31
  for S being MetrSpace, p,q,r being Element of S st q is_between p,r
  holds (not p is_between q,r) & not r is_between p,q;

theorem :: METRIC_1:32
  for S being MetrSpace, p,q,r,s being Element of S st q is_between p,r
  & r is_between p,s holds q is_between p,s & r is_between q,s;

definition
  let M be non empty MetrStruct, p,r be Element of M;
  func open_dist_Segment(p,r) -> Subset of M equals
:: METRIC_1:def 23
  {q where q is Element of M : q is_between p,r};
end;

theorem :: METRIC_1:33
  for M being non empty MetrSpace, p,r,x being Element of M holds
  x in open_dist_Segment(p,r) iff x is_between p,r;

definition
  let M be non empty MetrStruct, p,r be Element of M;
  func close_dist_Segment(p,r) -> Subset of M equals
:: METRIC_1:def 24
  {q where q is Element of M : q is_between p,r} \/ {p,r};
end;

theorem :: METRIC_1:34
  for M being non empty MetrStruct, p,r,x being Element of M holds
  x in close_dist_Segment(p,r) iff (x is_between p,r or x = p or x = r);