:: On Pseudometric Spaces :: by Adam Lecko and Mariusz Startek :: :: Received September 28, 1990 :: Copyright (c) 1990-2021 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;