:: 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; theorems TARSKI, BINOP_1, METRIC_1, SUBSET_1, MCART_1, XBOOLE_0, XXREAL_0, XREAL_0; schemes FRAENKEL, BINOP_1; begin :: Equivalence classes definition let M be non empty MetrStruct, x,y be Element of M; pred x tolerates y means 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 by METRIC_1:1; end; definition let M be symmetric non empty MetrStruct, x, y be Element of M; redefine pred x tolerates y; symmetry proof let x, y be Element of M; assume x tolerates y; then dist(x,y) = 0; hence thesis; end; end; definition let M be non empty MetrStruct, x be Element of M; func x-neighbour -> Subset of M equals {y where y is Element of M: x tolerates y}; coherence proof defpred P[Element of M] means x tolerates \$1; {y where y is Element of M: P[y]} c= the carrier of M from FRAENKEL: sch 10; hence thesis; end; end; definition let M be non empty MetrStruct; mode equivalence_class of M -> Subset of M means :Def3: ex x being Element of M st it=x-neighbour; existence proof set z = the Element of M; z-neighbour is Subset of M; hence thesis; end; end; Lm1: for M being Reflexive non empty MetrStruct, x being Element of M holds x tolerates x; theorem Th1: for M being PseudoMetricSpace, x,y,z being Element of M holds x tolerates y & y tolerates z implies x tolerates z proof let M be PseudoMetricSpace, x,y,z be Element of M; assume x tolerates y & y tolerates z; then dist(x,y)=0 & dist(y,z)=0; then dist(x,z) <= 0 + 0 by METRIC_1:4; then dist(x,z) = 0 by METRIC_1:5; hence thesis; end; theorem Th2: for M being PseudoMetricSpace,x,y being Element of M holds y in x -neighbour iff y tolerates x proof let M be PseudoMetricSpace,x,y be Element of M; hereby assume y in x-neighbour; then ex q be Element of M st y = q & x tolerates q; hence y tolerates x; end; assume y tolerates x; hence thesis; end; theorem for M being PseudoMetricSpace,x,p,q being Element of M st p in x-neighbour & q in x-neighbour holds p tolerates q proof let M be PseudoMetricSpace, x,p,q be Element of M; assume p in x-neighbour & q in x-neighbour; then p tolerates x & q tolerates x by Th2; hence thesis by Th1; end; theorem Th4: for M being PseudoMetricSpace, x being Element of M holds x in x-neighbour proof let M be PseudoMetricSpace, x be Element of M; x tolerates x by Lm1; hence thesis; end; theorem for M being PseudoMetricSpace, x,y being Element of M holds x in y-neighbour implies y in x-neighbour proof let M be PseudoMetricSpace, x,y be Element of M; assume x in y-neighbour; then x tolerates y by Th2; hence thesis; end; theorem for M being PseudoMetricSpace, p,x,y being Element of M holds p in x -neighbour & x tolerates y implies p in y-neighbour proof let M be PseudoMetricSpace,p,x,y be Element of M; assume that A1: p in x-neighbour and A2: x tolerates y; p tolerates x by A1,Th2; then p tolerates y by A2,Th1; hence thesis; end; theorem Th7: for M being PseudoMetricSpace, x,y being Element of M holds y in x-neighbour implies x-neighbour = y-neighbour proof let M be PseudoMetricSpace, x,y be Element of M; assume A1: y in x-neighbour; for p being Element of M holds p in y-neighbour implies p in x -neighbour proof let p be Element of M; assume p in y-neighbour; then A2: p tolerates y by Th2; y tolerates x by A1,Th2; then p tolerates x by A2,Th1; hence thesis; end; then A3: y-neighbour c= x-neighbour by SUBSET_1:2; for p being Element of M holds p in x-neighbour implies p in y-neighbour proof let p be Element of M; assume p in x-neighbour; then A4: p tolerates x by Th2; x tolerates y by A1,Th2; then p tolerates y by A4,Th1; hence thesis; end; then x-neighbour c= y-neighbour by SUBSET_1:2; hence thesis by A3,XBOOLE_0:def 10; end; theorem Th8: for M being PseudoMetricSpace, x,y being Element of M holds x-neighbour = y-neighbour iff x tolerates y by Th2,Th4,Th7; theorem for M being PseudoMetricSpace, x,y being Element of M holds x-neighbour meets y-neighbour iff x tolerates y proof let M be PseudoMetricSpace, x,y be Element of M; hereby assume x-neighbour meets y-neighbour; then consider p being object such that A1: p in x-neighbour and A2: p in y-neighbour by XBOOLE_0:3; A3: ex q being Element of M st q=p & x tolerates q by A1; reconsider p as Element of M by A1; ex s being Element of M st s=p & y tolerates s by A2; hence x tolerates y by A3,Th1; end; assume x tolerates y; then A4: x in y-neighbour; x in x-neighbour by Th4; hence thesis by A4,XBOOLE_0:3; end; Lm2: for M being PseudoMetricSpace, V being equivalence_class of M holds V is non empty set proof let M be PseudoMetricSpace, V be equivalence_class of M; ex x being Element of M st V=x-neighbour by Def3; hence thesis by Th4; end; registration let M be PseudoMetricSpace; cluster -> non empty for equivalence_class of M; coherence by Lm2; end; theorem Th10: 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 proof let M be PseudoMetricSpace, x,p,q be Element of M; assume p in x-neighbour & q in x-neighbour; then p tolerates x & q tolerates x by Th2; then p tolerates q by Th1; hence thesis; end; theorem Th11: for M being Reflexive discerning non empty MetrStruct, x,y being Element of M holds x tolerates y iff x = y by METRIC_1:2; theorem Th12: for M being non empty MetrSpace,x,y being Element of M holds y in x-neighbour iff y = x proof let M be non empty MetrSpace, x,y be Element of M; hereby assume y in x-neighbour; then ex q be Element of M st y = q & x tolerates q; hence y = x by Th11; end; assume y = x; then x tolerates y by Th11; hence thesis; end; theorem Th13: for M being non empty MetrSpace,x being Element of M holds x -neighbour = {x} proof let M be non empty MetrSpace,x be Element of M; for p being Element of M holds p in {x} implies p in x -neighbour proof let p be Element of M; assume p in {x}; then p = x by TARSKI:def 1; hence thesis by Th12; end; then A1: {x} c= x-neighbour by SUBSET_1:2; for p being Element of M holds p in x-neighbour implies p in {x} proof let p be Element of M; assume p in x-neighbour; then p = x by Th12; hence thesis by TARSKI:def 1; end; then x-neighbour c= {x} by SUBSET_1:2; hence thesis by A1,XBOOLE_0:def 10; end; theorem 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}) proof let M be non empty MetrSpace, V be Subset of M; A1: V is equivalence_class of M implies ex x being Element of M st V={x} proof assume V is equivalence_class of M; then consider x being Element of M such that A2: V=x -neighbour by Def3; x-neighbour={x} by Th13; hence thesis by A2; end; (ex x being Element of M st V={x}) implies V is equivalence_class of M proof given x being Element of M such that A3: V={x}; {x}=x-neighbour by Th13; hence thesis by A3,Def3; end; hence thesis by A1; end; :: Set of the equivalence classes definition let M be non empty MetrStruct; func M-neighbour -> set equals {s where s is Subset of M: ex x being Element of M st x-neighbour = s}; coherence; end; registration let M be non empty MetrStruct; cluster M-neighbour -> non empty; coherence proof set y = the Element of M; y-neighbour in {s where s is Subset of M: ex x being Element of M st x -neighbour = s}; hence thesis; end; end; reserve V for set; theorem Th15: for M being non empty MetrStruct holds V in M-neighbour iff ex x being Element of M st V=x -neighbour proof let M be non empty MetrStruct; V in M-neighbour implies ex x being Element of M st V=x -neighbour proof assume V in M-neighbour; then ex q being Subset of M st (q=V & ex x being Element of M st q=x -neighbour ); hence thesis; end; hence thesis; end; theorem for M being non empty MetrStruct, x being Element of M holds x -neighbour in M-neighbour; theorem Th17: for M being non empty MetrStruct holds V in M-neighbour iff V is equivalence_class of M proof let M be non empty MetrStruct; A1: V is equivalence_class of M implies V in M-neighbour proof assume V is equivalence_class of M; then ex x being Element of M st V=x-neighbour by Def3; hence thesis; end; V in M-neighbour implies V is equivalence_class of M proof assume V in M-neighbour; then ex x being Element of M st V=x-neighbour by Th15; hence thesis by Def3; end; hence thesis by A1; end; theorem for M being non empty MetrSpace, x being Element of M holds {x} in M-neighbour proof let M be non empty MetrSpace,x be Element of M; x-neighbour = {x} by Th13; hence thesis; end; theorem for M being non empty MetrSpace holds V in M-neighbour iff ex x being Element of M st V={x} proof let M be non empty MetrSpace; A1: V in M-neighbour implies ex x being Element of M st V={x} proof assume V in M-neighbour; then consider x being Element of M such that A2: V=x -neighbour by Th15; x-neighbour = {x} by Th13; hence thesis by A2; end; (ex x being Element of M st V={x}) implies V in M-neighbour proof given x being Element of M such that A3: V={x}; x-neighbour = {x} by Th13; hence thesis by A3; end; hence thesis by A1; end; theorem Th20: 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)) proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour; let p1,p2,q1,q2 be Element of M; assume that A1: p1 in V and A2: q1 in Q and A3: p2 in V and A4: q2 in Q; V is equivalence_class of M by Th17; then ex x being Element of M st V=x-neighbour by Def3; then A5: dist(p1,p2)=0 by A1,A3,Th10; Q is equivalence_class of M by Th17; then ex y being Element of M st Q=y-neighbour by Def3; then A6: dist(q1,q2)=0 by A2,A4,Th10; dist(p2,q2) <= dist(p2,p1) + dist(p1,q2) & dist(p1,q2) <= dist(p1,q1) + dist (q1,q2) by METRIC_1:4; then A7: dist(p2,q2) <= dist(p1,q1) by A5,A6,XXREAL_0:2; dist(p1,q1) <= dist(p1,p2) + dist(p2,q1) & dist(p2,q1) <= dist(p2,q2) + dist (q2,q1) by METRIC_1:4; then dist(p1,q1) <= dist(p2,q2) by A5,A6,XXREAL_0:2; hence thesis by A7,XXREAL_0:1; end; definition let M be non empty MetrStruct, V, Q be Element of M-neighbour, v be Real; pred V,Q is_dst v means for p,q being Element of M st p in V & q in Q holds dist(p,q)=v; end; theorem Th21: 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 proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour, v be Real; A1: V,Q is_dst v implies ex p,q being Element of M st p in V & q in Q & dist (p,q)=v proof consider q being Element of M such that A2: Q=q-neighbour by Th15; A3: q in Q by A2,Th4; assume A4: V,Q is_dst v; consider p being Element of M such that A5: V=p-neighbour by Th15; p in V by A5,Th4; then dist(p,q)=v by A4,A3; hence thesis by A5,A3,Th4; end; (ex p,q being Element of M st (p in V & q in Q & dist(p,q)=v)) implies V ,Q is_dst v by Th20; hence thesis by A1; end; theorem Th22: 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 proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour, v be Element of REAL; assume V,Q is_dst v; then for q,p being Element of M st q in Q & p in V holds dist(q,p)=v; hence thesis; end; definition let M be non empty MetrStruct, V,Q be Element of M-neighbour; func ev_eq_1(V,Q) -> Subset of REAL equals {v where v is Element of REAL: V, Q is_dst v}; coherence proof defpred P[Element of REAL] means V,Q is_dst \$1; {v where v is Element of REAL: P[v]} c= REAL from FRAENKEL:sch 10; hence thesis; end; end; theorem 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 proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour , v be Element of REAL; v in ev_eq_1(V,Q) implies V,Q is_dst v proof assume v in ev_eq_1(V,Q); then ex r being Element of REAL st r=v & V,Q is_dst r; hence thesis; end; hence thesis; end; 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 {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}; coherence proof defpred P[Element of [:M-neighbour,M-neighbour:]] means ex V,Q being Element of M-neighbour st \$1=[V,Q] & V,Q is_dst v; {W where W is Element of [:M-neighbour,M-neighbour :]: P[W] } c= [:M -neighbour,M-neighbour :] from FRAENKEL:sch 10; hence thesis; end; end; theorem 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 proof let M be PseudoMetricSpace, v be Element of REAL, W be Element of [:M -neighbour,M-neighbour:]; W in ev_eq_2(v,M) implies ex V,Q being Element of M-neighbour st W=[V,Q] & V,Q is_dst v proof assume W in ev_eq_2(v,M); then ex S being Element of [:M-neighbour,M-neighbour:] st W = S & ex V,Q being Element of M-neighbour st S=[V,Q] & V,Q is_dst v; hence thesis; end; hence thesis; end; definition let M be non empty MetrStruct; func real_in_rel M -> Subset of REAL equals {v where v is Element of REAL: ex V,Q being Element of M-neighbour st (V,Q is_dst v)}; coherence proof defpred P[Element of REAL] means ex V,Q being Element of M-neighbour st V, Q is_dst \$1; {v where v is Element of REAL:P[v]} c= REAL from FRAENKEL:sch 10; hence thesis; end; end; theorem 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 proof let M be PseudoMetricSpace, v be Element of REAL; v in real_in_rel M implies ex V,Q being Element of M-neighbour st V,Q is_dst v proof assume v in real_in_rel M; then ex r be Element of REAL st v=r & ex V,Q being Element of M-neighbour st V,Q is_dst r; hence thesis; end; hence thesis; end; definition let M be non empty MetrStruct; func elem_in_rel_1 M -> Subset of M-neighbour equals {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}; coherence proof defpred P[Element of M-neighbour] means ex Q being Element of M-neighbour, v being Element of REAL st \$1,Q is_dst v; {V where V is Element of M-neighbour: P[V] } c= M-neighbour from FRAENKEL:sch 10; hence thesis; end; end; theorem Th26: 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 proof let M be PseudoMetricSpace, V be Element of M-neighbour; V in elem_in_rel_1 M implies ex Q being Element of M-neighbour , v being Element of REAL st V,Q is_dst v proof assume V in elem_in_rel_1 M; then ex S being Element of M-neighbour st S=V & ex Q being Element of M -neighbour , v being Element of REAL st S,Q is_dst v; hence thesis; end; hence thesis; end; definition let M be non empty MetrStruct; func elem_in_rel_2 M -> Subset of M-neighbour equals {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}; coherence proof defpred P[Element of M-neighbour] means ex V being Element of M-neighbour, v being Element of REAL st V,\$1 is_dst v; {Q where Q is Element of M-neighbour: P[Q]} c= M-neighbour from FRAENKEL:sch 10; hence thesis; end; end; theorem Th27: 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 proof let M be PseudoMetricSpace, Q be Element of M-neighbour; Q in elem_in_rel_2 M implies ex V being Element of M-neighbour , v being Element of REAL st V,Q is_dst v proof assume Q in elem_in_rel_2 M; then ex S being Element of M-neighbour st S=Q & ex V being Element of M -neighbour , v being Element of REAL st V,S is_dst v; hence thesis; end; hence thesis; end; definition let M be non empty MetrStruct; func elem_in_rel M -> Subset of [:M-neighbour,M-neighbour:] equals {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}; coherence proof defpred P[Element of [:M-neighbour,M-neighbour:]] means ex V,Q being Element of M-neighbour, v being Element of REAL st \$1 = [V,Q] & V,Q is_dst v; {VQ where VQ is Element of [:M-neighbour,M-neighbour:]: P[VQ] } c= [:M -neighbour,M-neighbour:] from FRAENKEL:sch 10; hence thesis; end; end; theorem 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 proof let M be PseudoMetricSpace, VQ be Element of [:M-neighbour,M-neighbour:]; VQ in elem_in_rel M implies ex V,Q being Element of M-neighbour, v being Element of REAL st VQ = [V,Q] & V,Q is_dst v proof assume VQ in elem_in_rel M; then ex S being Element of [:M-neighbour,M-neighbour:] st VQ=S & ex V,Q being Element of M-neighbour, v being Element of REAL st S = [V,Q] & V,Q is_dst v; hence thesis; end; hence thesis; end; definition let M be non empty MetrStruct; func set_in_rel M -> Subset of [:M-neighbour,M-neighbour,REAL:] equals {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}; coherence proof defpred P[Element of [:M-neighbour,M-neighbour,REAL:]] means ex V,Q being Element of M-neighbour,v being Element of REAL st \$1 = [V,Q,v] & V,Q is_dst v; {VQv where VQv is Element of [:M-neighbour,M-neighbour,REAL:]: P[VQv] } c= [:M-neighbour,M-neighbour,REAL:] from FRAENKEL:sch 10; hence thesis; end; end; theorem Th29: 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 proof let M be PseudoMetricSpace,VQv be Element of [:M-neighbour,M-neighbour ,REAL :]; VQv in set_in_rel M implies ex V,Q being Element of M-neighbour,v being Element of REAL st VQv = [V,Q,v] & V,Q is_dst v proof assume VQv in set_in_rel M; then ex S being Element of [:M-neighbour,M-neighbour,REAL:] st VQv = S & ex V,Q being Element of M-neighbour,v being Element of REAL st S = [V,Q,v] & V,Q is_dst v; hence thesis; end; hence thesis; end; theorem for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M proof let M be PseudoMetricSpace; for V being Element of M-neighbour holds (V in elem_in_rel_2 M implies V in elem_in_rel_1 M) proof let V be Element of M-neighbour; assume V in elem_in_rel_2 M; then consider Q being Element of M-neighbour, v being Element of REAL such that A1: Q,V is_dst v by Th27; V,Q is_dst v by A1,Th22; hence thesis; end; then A2: elem_in_rel_2 M c= elem_in_rel_1 M by SUBSET_1:2; for V being Element of M-neighbour holds (V in elem_in_rel_1 M implies V in elem_in_rel_2 M) proof let V be Element of M-neighbour; assume V in elem_in_rel_1 M; then consider Q being Element of M-neighbour, v being Element of REAL such that A3: V,Q is_dst v by Th26; Q,V is_dst v by A3,Th22; hence thesis; end; then elem_in_rel_1 M c= elem_in_rel_2 M by SUBSET_1:2; hence thesis by A2,XBOOLE_0:def 10; end; theorem for M being PseudoMetricSpace holds set_in_rel M c= [:elem_in_rel_1 M, elem_in_rel_2 M,real_in_rel M:] proof let M be PseudoMetricSpace; for VQv being Element of [:M-neighbour,M-neighbour ,REAL:] holds (VQv in set_in_rel M implies VQv in [:elem_in_rel_1 M,elem_in_rel_2 M,real_in_rel M:]) proof let VQv be Element of [:M-neighbour,M-neighbour,REAL:]; assume VQv in set_in_rel M; then consider V,Q being Element of M-neighbour ,v being Element of REAL such that A1: VQv = [V,Q,v] and A2: V,Q is_dst v by Th29; A3: v in real_in_rel M by A2; V in elem_in_rel_1 M & Q in elem_in_rel_2 M by A2; hence thesis by A1,A3,MCART_1:69; end; hence thesis by SUBSET_1:2; end; theorem 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 proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour , v1,v2 be Element of REAL; assume that A1: V,Q is_dst v1 and A2: V,Q is_dst v2; consider p1 being Element of M such that A3: V=p1-neighbour by Th15; consider q1 being Element of M such that A4: Q=q1-neighbour by Th15; A5: q1 in Q by A4,Th4; A6: p1 in V by A3,Th4; then dist(p1,q1)=v1 by A1,A5; hence thesis by A2,A6,A5; end; theorem Th33: for M being PseudoMetricSpace, V,Q being Element of M-neighbour ex v being Real st V,Q is_dst v proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour; consider p being Element of M such that A1: V=p-neighbour by Th15; consider q being Element of M such that A2: Q=q-neighbour by Th15; A3: q in Q by A2,Th4; p in V by A1,Th4; then V,Q is_dst (dist(p,q)) by A3,Th21; hence thesis; end; definition let M be PseudoMetricSpace; func nbourdist M -> Function of [:M-neighbour,M-neighbour:],REAL means :Def13: 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); existence proof defpred P[Element of M-neighbour,Element of M-neighbour,Real] means \$1,\$2 is_dst \$3; A1: for V,Q being Element of M-neighbour holds ex v being Element of REAL st P[V,Q,v] proof let V,Q being Element of M-neighbour; consider v being Real such that A2: P[V,Q,v] by Th33; reconsider v as Element of REAL by XREAL_0:def 1; take v; thus thesis by A2; end; consider F being Function of [:M-neighbour,M-neighbour:],REAL such that A3: for V,Q being Element of M-neighbour holds P[V,Q,F.(V,Q)] from BINOP_1:sch 3(A1); take F; let V,Q be Element of M-neighbour , p,q be Element of M such that A4: p in V & q in Q; V,Q is_dst F.(V,Q) by A3; hence thesis by A4; end; uniqueness proof let F1,F2 be Function of [:M-neighbour,M-neighbour:],REAL; assume that A5: for V,Q being Element of M-neighbour for p,q being Element of M st p in V & q in Q holds F1.(V,Q)=dist(p,q) and A6: for V,Q being Element of M-neighbour for p,q being Element of M st p in V & q in Q holds F2.(V,Q)=dist(p,q); for V,Q being Element of M-neighbour holds F1.(V,Q) = F2.(V,Q) proof let V,Q be Element of M-neighbour; consider p being Element of M such that A7: V=p-neighbour by Th15; consider q being Element of M such that A8: Q=q-neighbour by Th15; A9: q in Q by A8,Th4; A10: p in V by A7,Th4; then F1.(V,Q) = dist(p,q) by A5,A9 .= F2.(V,Q) by A6,A10,A9; hence thesis; end; hence thesis by BINOP_1:2; end; end; theorem Th34: for M being PseudoMetricSpace, V,Q being Element of M-neighbour holds (nbourdist M).(V,Q) = 0 iff V = Q proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour; A1: V=Q implies (nbourdist M).(V,Q) = 0 proof consider p being Element of M such that A2: V=p-neighbour by Th15; A3: p in V by A2,Th4; consider q being Element of M such that A4: Q=q-neighbour by Th15; assume V = Q; then A5: p tolerates q by A3,A4,Th2; q in Q by A4,Th4; then (nbourdist M).(V,Q) = dist(p,q) by A3,Def13 .= 0 by A5; hence thesis; end; (nbourdist M).(V,Q) = 0 implies V = Q proof assume A6: (nbourdist M).(V,Q) = 0; consider p being Element of M such that A7: V=p-neighbour by Th15; consider q being Element of M such that A8: Q=q-neighbour by Th15; A9: q in Q by A8,Th4; p in V by A7,Th4; then dist(p,q) = 0 by A6,A9,Def13; then p tolerates q; hence thesis by A7,A8,Th8; end; hence thesis by A1; end; theorem Th35: for M being PseudoMetricSpace, V,Q being Element of M-neighbour holds (nbourdist M).(V,Q) = (nbourdist M).(Q,V) proof let M be PseudoMetricSpace, V,Q be Element of M-neighbour; consider p being Element of M such that A1: V=p-neighbour by Th15; consider q being Element of M such that A2: Q=q-neighbour by Th15; A3: q in Q by A2,Th4; A4: p in V by A1,Th4; then (nbourdist M).(V,Q) = dist(q,p) by A3,Def13 .= (nbourdist M).(Q,V) by A4,A3,Def13; hence thesis; end; theorem Th36: 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) proof let M be PseudoMetricSpace,V,Q,W be Element of M-neighbour; consider p being Element of M such that A1: V=p-neighbour by Th15; consider w being Element of M such that A2: W=w-neighbour by Th15; A3: w in W by A2,Th4; consider q being Element of M such that A4: Q=q-neighbour by Th15; A5: q in Q by A4,Th4; then A6: (nbourdist M).(Q,W) = dist(q,w) by A3,Def13; A7: p in V by A1,Th4; then A8: (nbourdist M).(V,W) = dist(p,w) by A3,Def13; (nbourdist M).(V,Q) = dist(p,q) by A7,A5,Def13; hence thesis by A8,A6,METRIC_1:4; end; definition let M be PseudoMetricSpace; func Eq_classMetricSpace M -> MetrSpace equals MetrStruct(#M-neighbour, nbourdist M#); coherence proof set Z = MetrStruct(#M-neighbour,nbourdist M#); now let V,Q,W be Element of Z; reconsider V9=V, Q9=Q,W9=W as Element of M-neighbour; A1: dist(V,Q) = (nbourdist M).(V9,Q9) by METRIC_1:def 1; hence dist(V,Q)=0 iff V=Q by Th34; dist(Q,V) = (nbourdist M).(Q9,V9) by METRIC_1:def 1; hence dist(V,Q) = dist(Q,V) by A1,Th35; dist(V,W) = (nbourdist M).(V9,W9) & dist(Q,W) = (nbourdist M).(Q9,W9 ) by METRIC_1:def 1; hence dist(V,W) <= dist(V,Q) + dist(Q,W) by A1,Th36; end; hence thesis by METRIC_1:6; end; end; registration let M be PseudoMetricSpace; cluster Eq_classMetricSpace M -> strict non empty; coherence; end;