The abstract of the Mizar article:

On Pseudometric Spaces

by

Adam Lecko, and

Mariusz Startek

Received September 28, 1990

MML identifier: METRIC_2

[ Mizar article, MML identifier index ]

environ

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


begin :: Equivalence classes

definition let M be non empty MetrStruct, x,y be Element of M;
  pred x tolerates y means
:: METRIC_2:def 1
    dist(x,y)=0;
end;

definition let M be Reflexive (non empty MetrStruct),
               x, y be Element of M;
  redefine pred x tolerates y;
  reflexivity;
end;

definition let M be symmetric (non empty MetrStruct),
               x, y be Element of M;
  redefine pred x tolerates y;
  symmetry;
end;

definition let M be non empty MetrStruct, x be Element of M;
   func x-neighbour -> Subset of M equals
:: METRIC_2:def 2
     {y where y is Element of M: x tolerates y};
end;

definition let M be non empty MetrStruct;
  mode equivalence_class of M -> Subset of M means
:: METRIC_2:def 3
    ex x being Element of M st it=x-neighbour;
   end;

canceled 5;

theorem :: METRIC_2:6
   for M being PseudoMetricSpace,
    x,y,z being Element of M holds
               (x tolerates y & y tolerates z) implies x tolerates z;

theorem :: METRIC_2:7
   for M being PseudoMetricSpace,x,y being Element of M
        holds y in x-neighbour iff y tolerates x;

theorem :: METRIC_2:8
    for M being PseudoMetricSpace,x,p,q being Element of M
           holds p in x-neighbour & q in x-neighbour implies p tolerates q;

theorem :: METRIC_2:9
   for M being PseudoMetricSpace, x being Element of M
            holds x in x-neighbour;

theorem :: METRIC_2:10
     for M being PseudoMetricSpace, x,y being Element of M
         holds x in y-neighbour iff y in x-neighbour;

theorem :: METRIC_2:11
     for M being PseudoMetricSpace, p,x,y being Element of M
         holds p in x-neighbour & x tolerates y implies p in y-neighbour;

theorem :: METRIC_2:12
   for M being PseudoMetricSpace, x,y being Element of M
            holds y in x-neighbour implies x-neighbour = y-neighbour;

theorem :: METRIC_2:13
   for M being PseudoMetricSpace,
            x,y being Element of M
              holds x-neighbour = y-neighbour iff x tolerates y;

theorem :: METRIC_2:14
     for M being PseudoMetricSpace, x,y being Element of M
           holds x-neighbour meets y-neighbour iff x tolerates y;

canceled;

theorem :: METRIC_2:16
   for M being PseudoMetricSpace, V being equivalence_class of M holds
     V is non empty set;

definition let M be PseudoMetricSpace;
  cluster -> non empty equivalence_class of M;
end;

theorem :: METRIC_2:17
  for M being PseudoMetricSpace, x,p,q being Element of M
              holds
            (p in x-neighbour & q in x-neighbour) implies dist(p,q)=0;

::----------------------------------------------------------------------------

theorem :: METRIC_2:18
   for M being Reflexive discerning (non empty MetrStruct),
     x,y being Element of M holds
              x tolerates y iff x = y;

theorem :: METRIC_2:19
 for M being non empty MetrSpace,x,y being Element of M holds
   y in x-neighbour iff y = x;

theorem :: METRIC_2:20
   for M being non empty MetrSpace,x being Element of M
                    holds
            x-neighbour = {x};

theorem :: METRIC_2:21
     for M being non empty MetrSpace, V being Subset of M
               holds
             (V is equivalence_class of M iff
             ex x being Element of M st V={x});

:: Set of the equivalence classes

definition let M be non empty MetrStruct;
  func M-neighbour -> set equals
:: METRIC_2:def 4
    {s where s is Element of bool the carrier of M:
                 ex x being Element of M st x-neighbour = s};
end;

definition let M be non empty MetrStruct;
  cluster M-neighbour -> non empty;
end;

 reserve V for set;

canceled;

theorem :: METRIC_2:23
   for M being non empty MetrStruct holds
            V in M-neighbour iff ex x being Element of M st V=x
-neighbour;

theorem :: METRIC_2:24
    for M being non empty MetrStruct,
  x being Element of M holds
            x-neighbour in M-neighbour;

canceled;

theorem :: METRIC_2:26
   for M being non empty MetrStruct holds
            V in M-neighbour iff V is equivalence_class of M;

theorem :: METRIC_2:27
    for M being non empty MetrSpace, x being Element of M holds
   {x} in M-neighbour;

theorem :: METRIC_2:28
     for M being non empty MetrSpace holds
     V in M-neighbour iff ex x being Element of M st V={x};

theorem :: METRIC_2:29
    for M being PseudoMetricSpace, V,Q being Element of M-neighbour
             for p1,p2,q1,q2 being Element of M
                 holds
    ((p1 in V & q1 in Q & p2 in V & q2 in Q) implies dist(p1,q1)=dist(p2,q2));

definition let M be non empty MetrStruct,
               V, Q be Element of M-neighbour,
               v be Element of REAL;
  pred V,Q is_dst v means
:: METRIC_2:def 5
    for p,q being Element of M st (p in V & q in Q)
                  holds dist(p,q)=v;
end;

canceled;

theorem :: METRIC_2:31
   for M being PseudoMetricSpace, V,Q being Element of M-neighbour,
            v being Element of REAL holds
           V,Q is_dst v iff (ex p,q being Element of M
                       st (p in V & q in Q & dist(p,q)=v));

theorem :: METRIC_2:32
   for M being PseudoMetricSpace, V,Q being Element of M-neighbour,
       v being Element of REAL holds V,Q is_dst v iff Q,V is_dst v;

definition let M be non empty MetrStruct,
               V,Q be Element of M-neighbour;
  func ev_eq_1(V,Q) -> Subset of REAL equals
:: METRIC_2:def 6
      {v where v is Element of REAL: V,Q is_dst v};
    end;

canceled;

theorem :: METRIC_2:34
     for M being PseudoMetricSpace, V,Q being Element of M-neighbour,
       v being Element of REAL holds
     v in ev_eq_1(V,Q) iff V,Q is_dst v;

definition let M be non empty MetrStruct, v be Element of REAL;
  func ev_eq_2(v,M) -> Subset of [:M-neighbour,M-neighbour:] equals
:: METRIC_2:def 7
      {W where W is Element of [:M-neighbour,M-neighbour:]:
                   ex V,Q being Element of M-neighbour
 st W=[V,Q] & V,Q is_dst v};
     end;

canceled;

theorem :: METRIC_2:36
     for M being PseudoMetricSpace, v being Element of REAL,
               W being Element of [:M-neighbour,M-neighbour:] holds
           W in ev_eq_2(v,M) iff
           (ex V,Q being Element of M-neighbour st W=[V,Q] & V,Q is_dst v);

definition let M be non empty MetrStruct;
  func real_in_rel M -> Subset of REAL equals
:: METRIC_2:def 8
    {v where v is Element of REAL: ex V,Q being Element of M-neighbour st
                 (V,Q is_dst v)};
  end;

canceled;

theorem :: METRIC_2:38
   for M being PseudoMetricSpace, v being Element of REAL holds
    v in
 real_in_rel M iff (ex V,Q being Element of M-neighbour st V,Q is_dst v);

definition let M be non empty MetrStruct;
  func elem_in_rel_1 M -> Subset of M-neighbour equals
:: METRIC_2:def 9
    {V where V is Element of M-neighbour:
           ex Q being Element of M-neighbour
, v being Element of REAL st V,Q is_dst v};
  end;

canceled;

theorem :: METRIC_2:40
   for M being PseudoMetricSpace, V being Element of M-neighbour
              holds
          V in elem_in_rel_1 M iff
          (ex Q being Element of M-neighbour
, v being Element of REAL st V,Q is_dst v);

definition let M be non empty MetrStruct;
  func elem_in_rel_2 M -> Subset of M-neighbour equals
:: METRIC_2:def 10
    {Q where Q is Element of M-neighbour:
           ex V being Element of M-neighbour
, v being Element of REAL st V,Q is_dst v};
  end;

canceled;

theorem :: METRIC_2:42
   for M being PseudoMetricSpace, Q being Element of M-neighbour
              holds
          Q in elem_in_rel_2 M iff
          (ex V being Element of M-neighbour
, v being Element of REAL st V,Q is_dst v);

definition let M be non empty MetrStruct;
  func elem_in_rel M -> Subset of [:M-neighbour,M-neighbour:] equals
:: METRIC_2:def 11
    {V_Q where V_Q is Element of [:M-neighbour,M-neighbour:]:
                   ex V,Q being Element of M-neighbour, v being Element of REAL
                   st V_Q = [V,Q] & V,Q is_dst v};
  end;

canceled;

theorem :: METRIC_2:44
     for M being PseudoMetricSpace, V_Q being Element of [:M-neighbour,M
-neighbour:]
             holds
           V_Q in elem_in_rel M iff
           (ex V,Q being Element of M-neighbour, v being Element of REAL
                   st V_Q = [V,Q] & V,Q is_dst v);

definition let M be non empty MetrStruct;
  func set_in_rel M -> Subset of [:M-neighbour,M-neighbour,REAL:] equals
:: METRIC_2:def 12
    {V_Q_v where V_Q_v is Element of [:M-neighbour,M-neighbour,REAL:]:
                  ex V,Q being Element of M-neighbour
,v being Element of REAL st
                  V_Q_v = [V,Q,v] & V,Q is_dst v};
  end;

canceled;

theorem :: METRIC_2:46
   for M being PseudoMetricSpace,V_Q_v being Element of [:M-neighbour,M
-neighbour,REAL:]
              holds
            V_Q_v in set_in_rel M iff
            (ex V,Q being Element of M-neighbour,v being Element of REAL st
                  V_Q_v = [V,Q,v] & V,Q is_dst v);

theorem :: METRIC_2:47
     for M being PseudoMetricSpace holds
          elem_in_rel_1 M = elem_in_rel_2 M;

theorem :: METRIC_2:48
     for M being PseudoMetricSpace holds
        set_in_rel M c= [:elem_in_rel_1 M,elem_in_rel_2 M,real_in_rel M:];

canceled;

theorem :: METRIC_2:50
      for M being PseudoMetricSpace, V,Q being Element of M-neighbour,
                 v1,v2 being Element of REAL
                     holds
              ((V,Q is_dst v1) & (V,Q is_dst v2)) implies v1=v2;

canceled;

theorem :: METRIC_2:52
    for M being PseudoMetricSpace, V,Q being Element of M-neighbour holds
                  ex v being Element of REAL st V,Q is_dst v;

definition let M be PseudoMetricSpace;
  func nbourdist M -> Function of [:M-neighbour,M-neighbour:],REAL means
:: METRIC_2:def 13
   for V,Q being Element of M-neighbour
              for p,q being Element of M st p in V & q in Q
              holds it.(V,Q)=dist(p,q);
  end;

canceled;

theorem :: METRIC_2:54
   for M being PseudoMetricSpace, V,Q being Element of M-neighbour holds
           (nbourdist M).(V,Q) = 0 iff V = Q;

theorem :: METRIC_2:55
   for M being PseudoMetricSpace, V,Q being Element of M-neighbour holds
           (nbourdist M).(V,Q) = (nbourdist M).(Q,V);

theorem :: METRIC_2:56
   for M being PseudoMetricSpace, V,Q,W being Element of M-neighbour holds
           (nbourdist M).(V,W) <= (nbourdist M).(V,Q) + (nbourdist M).(Q,W);

definition let M be PseudoMetricSpace;
  func Eq_classMetricSpace M -> MetrSpace equals
:: METRIC_2:def 14
    MetrStruct(#M-neighbour,nbourdist M#);
      end;

definition let M be PseudoMetricSpace;
  cluster Eq_classMetricSpace M -> strict non empty;
end;