The abstract of the Mizar article:

Submetric Spaces --- Part I

by

Adam Lecko, and

Mariusz Startek

Received September 27, 1990

MML identifier: SUB_METR

[ Mizar article, MML identifier index ]

environ

 vocabulary SQUARE_1, METRIC_1, BOOLE, FUNCT_1, RELAT_2, FUNCOP_1, RELAT_1,
      SUB_METR;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1, SQUARE_1,
      STRUCT_0, METRIC_1;
 constructors FUNCOP_1, DOMAIN_1, SQUARE_1, METRIC_1, REAL_1, MEMBERED,
      XBOOLE_0;
 clusters SUBSET_1, METRIC_1, METRIC_3, STRUCT_0, XREAL_0, FUNCOP_1, RELSET_1,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

theorem :: SUB_METR:1
  for x,y being Element of REAL holds
    (0 <= x & 0 <= y) implies max(x,y) <= x + y;

theorem :: SUB_METR:2
  for M being MetrSpace, x,y being Element of M holds
    x <> y implies 0 < dist(x,y);

canceled;

theorem :: SUB_METR:4
  for x,y being Element of {{}} holds
    x = y implies Empty^2-to-zero.(x,y) = 0;

theorem :: SUB_METR:5
  for x,y being Element of {{}} holds
    x <> y implies 0 < Empty^2-to-zero.(x,y);

theorem :: SUB_METR:6
  for x,y being Element of {{}} holds
    Empty^2-to-zero.(x,y) = Empty^2-to-zero.(y,x);

theorem :: SUB_METR:7
  for x,y,z being Element of {{}} holds
    Empty^2-to-zero.(x,z) <= Empty^2-to-zero.(x,y) + Empty^2-to-zero.(y,z);

theorem :: SUB_METR:8
  for x,y,z being Element of {{}} holds
    Empty^2-to-zero.(x,z) <= max(Empty^2-to-zero.(x,y),Empty^2-to-zero.(y,z));

definition
  mode PseudoMetricSpace is Reflexive symmetric triangle
    (non empty MetrStruct);
end;

definition let A be non empty set;
  let f be Function of [:A,A:], REAL;
  attr f is Discerning means
:: SUB_METR:def 1
    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
:: SUB_METR:def 2
   the distance of M is Discerning;
end;

canceled 5;

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

definition
  cluster MetrStruct(#{{}},Empty^2-to-zero#) -> Reflexive symmetric Discerning
    triangle;
end;

definition
  cluster Reflexive Discerning symmetric triangle (non empty MetrStruct);
end;

definition
  mode SemiMetricSpace is Reflexive Discerning symmetric
    (non empty MetrStruct);
end;

canceled;

theorem :: SUB_METR:16
    for M being Discerning (non empty MetrStruct),
      a,b being Element of M holds
    a <> b implies 0 < dist(a,b);

canceled;

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

definition
  mode NonSymmetricMetricSpace is Reflexive Discerning triangle
         (non empty MetrStruct);
end;

canceled 2;

theorem :: SUB_METR:21
   for M being Discerning (non empty MetrStruct),
      a, b being Element of M holds
       a <> b implies 0 < dist(a,b);

canceled;

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

definition let M be non empty MetrStruct;
 canceled;

  attr M is ultra means
:: SUB_METR:def 4
    for a, b, c being Element of M holds
     dist(a,c) <= max (dist(a,b),dist(b,c));
end;

definition
  cluster strict ultra Reflexive symmetric Discerning (non empty MetrStruct);
end;

definition
  mode UltraMetricSpace is ultra Reflexive symmetric Discerning
    (non empty MetrStruct);
end;

canceled 2;

theorem :: SUB_METR:26
   for M being Discerning (non empty MetrStruct),
                   a,b being Element of M holds
       a <> b implies 0 < dist(a,b);

definition
  cluster -> Discerning (non empty MetrSpace);
end;

canceled 2;

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

definition
  cluster -> triangle discerning UltraMetricSpace;
end;

definition
  func Set_to_zero -> Function of [:{{},{{}}},{{},{{}}}:],REAL equals
:: SUB_METR:def 5
    [:{{},{{}}},{{},{{}}}:] --> 0;
end;

canceled 9;

theorem :: SUB_METR:39
   [{},{}] in [:{{},{{}}},{{},{{}}}:] & [{},{{}}] in [:{{},{{}}},{{},{{}}}:] &
       [{{}},{}] in [:{{},{{}}},{{},{{}}}:] & [{{}},{{}}] in
 [:{{},{{}}},{{},{{}}}:];

theorem :: SUB_METR:40
  for x,y being Element of {{},{{}}} holds Set_to_zero.(x,y) = 0;

canceled;

theorem :: SUB_METR:42
  for x,y being Element of {{},{{}}} holds Set_to_zero.(x,y)=Set_to_zero.(y,x);

theorem :: SUB_METR:43
  for x,y,z being Element of {{},{{}}} holds
    Set_to_zero.(x,z) <= Set_to_zero.(x,y) + Set_to_zero.(y,z);

definition
  func ZeroSpace -> MetrStruct equals
:: SUB_METR:def 6
    MetrStruct(#{{},{{}}},Set_to_zero#);
end;

definition
  cluster ZeroSpace -> strict non empty;
end;

definition
  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
:: SUB_METR:def 7
    p <> q & p <> r & q <> r & dist(p,r) = dist(p,q) + dist(q,r);
end;

canceled 3;

theorem :: SUB_METR:47
    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 :: SUB_METR:48
   for S being MetrSpace, p,q,r being Element of S holds
   (q is_between p,r implies (not p is_between q,r) & not r is_between p,q);

theorem :: SUB_METR:49
    for S being MetrSpace, p,q,r,s being Element of S
            holds (q is_between p,r & r is_between p,s) implies
                   (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
:: SUB_METR:def 8
    {q where q is Element of M : q is_between p,r};
end;

canceled;

theorem :: SUB_METR:51
    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
:: SUB_METR:def 9
    {q where q is Element of M : q is_between p,r} \/ {p,r};
end;

canceled;

theorem :: SUB_METR:53
    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);

theorem :: SUB_METR:54
    for M being non empty MetrStruct,
      p,r being Element of M holds
    open_dist_Segment(p,r) c= close_dist_Segment(p,r);