Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### On Pseudometric Spaces

by
Mariusz Startek

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;

```