Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

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

Back to top