:: On Pseudometric Spaces
:: by Adam Lecko and Mariusz Startek
::
:: Received September 28, 1990
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, METRIC_1, SUBSET_1, PARTFUN1, CARD_1, RELAT_2,
TARSKI, STRUCT_0, XXREAL_0, ARYTM_3, ZFMISC_1, FUNCT_1, METRIC_2, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, FUNCT_2, BINOP_1, DOMAIN_1, STRUCT_0, METRIC_1, MCART_1,
XXREAL_0;
constructors DOMAIN_1, XXREAL_0, REAL_1, MEMBERED, METRIC_1, BINOP_1;
registrations SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, METRIC_1,
ORDINAL1;
requirements REAL, SUBSET, BOOLE, ARITHM, NUMERALS;
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;
theorem :: METRIC_2:1
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:2
for M being PseudoMetricSpace,x,y being Element of M holds y in x
-neighbour iff y tolerates x;
theorem :: METRIC_2:3
for M being PseudoMetricSpace,x,p,q being Element of M st
p in x-neighbour & q in x-neighbour holds p tolerates q;
theorem :: METRIC_2:4
for M being PseudoMetricSpace, x being Element of M holds x in x-neighbour;
theorem :: METRIC_2:5
for M being PseudoMetricSpace, x,y being Element of M holds
x in y-neighbour implies y in x-neighbour;
theorem :: METRIC_2:6
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:7
for M being PseudoMetricSpace, x,y being Element of M holds y in
x-neighbour implies x-neighbour = y-neighbour;
theorem :: METRIC_2:8
for M being PseudoMetricSpace, x,y being Element of M holds
x-neighbour = y-neighbour iff x tolerates y;
theorem :: METRIC_2:9
for M being PseudoMetricSpace, x,y being Element of M holds
x-neighbour meets y-neighbour iff x tolerates y;
registration
let M be PseudoMetricSpace;
cluster -> non empty for equivalence_class of M;
end;
theorem :: METRIC_2:10
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:11
for M being Reflexive discerning non empty MetrStruct, x,y
being Element of M holds x tolerates y iff x = y;
theorem :: METRIC_2:12
for M being non empty MetrSpace,x,y being Element of M holds y
in x-neighbour iff y = x;
theorem :: METRIC_2:13
for M being non empty MetrSpace,x being Element of M holds x -neighbour = {x}
;
theorem :: METRIC_2:14
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 Subset of M: ex x being Element of M st x-neighbour = s};
end;
registration
let M be non empty MetrStruct;
cluster M-neighbour -> non empty;
end;
reserve V for set;
theorem :: METRIC_2:15
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:16
for M being non empty MetrStruct, x being Element of M holds x
-neighbour in M-neighbour;
theorem :: METRIC_2:17
for M being non empty MetrStruct holds V in M-neighbour iff V is
equivalence_class of M;
theorem :: METRIC_2:18
for M being non empty MetrSpace, x being Element of M holds
{x} in M-neighbour;
theorem :: METRIC_2:19
for M being non empty MetrSpace holds V in M-neighbour iff ex x being
Element of M st V={x};
theorem :: METRIC_2:20
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 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;
theorem :: METRIC_2:21
for M being PseudoMetricSpace, V,Q being Element of M-neighbour,
v being 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:22
for M being PseudoMetricSpace, V,Q being Element of M-neighbour,
v being Element of REAL st V,Q is_dst v holds 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;
theorem :: METRIC_2:23
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;
theorem :: METRIC_2:24
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;
theorem :: METRIC_2:25
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;
theorem :: METRIC_2:26
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;
theorem :: METRIC_2:27
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
{VQ where
VQ is Element of [:M-neighbour,M-neighbour:]: ex V,Q being Element of M
-neighbour, v being Element of REAL st VQ = [V,Q] & V,Q is_dst v};
end;
theorem :: METRIC_2:28
for M being PseudoMetricSpace, VQ being Element of [:M-neighbour,M
-neighbour:] holds VQ in elem_in_rel M iff ex V,Q being Element of M-neighbour,
v being Element of REAL st VQ = [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
{VQv
where VQv is Element of [:M-neighbour,M-neighbour,REAL:]: ex V,Q being Element
of M-neighbour ,v being Element of REAL st VQv = [V,Q,v] & V,Q is_dst v};
end;
theorem :: METRIC_2:29
for M being PseudoMetricSpace,VQv being Element of [:M-neighbour
,M -neighbour,REAL:] holds VQv in set_in_rel M iff ex V,Q being Element of M
-neighbour,v being Element of REAL st VQv = [V,Q,v] & V,Q is_dst v;
theorem :: METRIC_2:30
for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M;
theorem :: METRIC_2:31
for M being PseudoMetricSpace holds set_in_rel M c= [:elem_in_rel_1 M,
elem_in_rel_2 M,real_in_rel M:];
theorem :: METRIC_2:32
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;
theorem :: METRIC_2:33
for M being PseudoMetricSpace, V,Q being Element of M-neighbour
ex v being 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;
theorem :: METRIC_2:34
for M being PseudoMetricSpace, V,Q being Element of M-neighbour
holds (nbourdist M).(V,Q) = 0 iff V = Q;
theorem :: METRIC_2:35
for M being PseudoMetricSpace, V,Q being Element of M-neighbour
holds (nbourdist M).(V,Q) = (nbourdist M).(Q,V);
theorem :: METRIC_2:36
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;
registration
let M be PseudoMetricSpace;
cluster Eq_classMetricSpace M -> strict non empty;
end;