Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

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

Back to top