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

### Submetric Spaces --- Part I

by
Mariusz Startek

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);
```