:: METRIC_2 semantic presentation begin definition let M be non empty MetrStruct ; let x, y be Element of M; predx tolerates y means :Def1: :: METRIC_2:def 1 dist (x,y) = 0 ; end; :: deftheorem Def1 defines tolerates METRIC_2:def_1_:_ for M being non empty MetrStruct for x, y being Element of M holds ( x tolerates y iff dist (x,y) = 0 ); definition let M be non empty Reflexive MetrStruct ; let x, y be Element of M; :: original: tolerates redefine predx tolerates y; reflexivity for x being Element of M holds (M,b1,b1) proof let x be Element of M; ::_thesis: (M,x,x) dist (x,x) = 0 by METRIC_1:1; hence (M,x,x) by Def1; ::_thesis: verum end; end; definition let M be non empty symmetric MetrStruct ; let x, y be Element of M; :: original: tolerates redefine predx tolerates y; symmetry for x, y being Element of M st (M,b1,b2) holds (M,b2,b1) proof let x, y be Element of M; ::_thesis: ( (M,x,y) implies (M,y,x) ) assume x tolerates y ; ::_thesis: (M,y,x) then dist (x,y) = 0 by Def1; hence (M,y,x) by Def1; ::_thesis: verum end; end; definition let M be non empty MetrStruct ; let x be Element of M; funcx -neighbour -> Subset of M equals :: METRIC_2:def 2 { y where y is Element of M : x tolerates y } ; coherence { y where y is Element of M : x tolerates y } is Subset of M proof defpred S1[ Element of M] means x tolerates \$1; { y where y is Element of M : S1[y] } c= the carrier of M from FRAENKEL:sch_10(); hence { y where y is Element of M : x tolerates y } is Subset of M ; ::_thesis: verum end; end; :: deftheorem defines -neighbour METRIC_2:def_2_:_ for M being non empty MetrStruct for x being Element of M holds x -neighbour = { y where y is Element of M : x tolerates y } ; definition let M be non empty MetrStruct ; mode equivalence_class of M -> Subset of M means :Def3: :: METRIC_2:def 3 ex x being Element of M st it = x -neighbour ; existence ex b1 being Subset of M ex x being Element of M st b1 = x -neighbour proof set z = the Element of M; the Element of M -neighbour is Subset of M ; hence ex b1 being Subset of M ex x being Element of M st b1 = x -neighbour ; ::_thesis: verum end; end; :: deftheorem Def3 defines equivalence_class METRIC_2:def_3_:_ for M being non empty MetrStruct for b2 being Subset of M holds ( b2 is equivalence_class of M iff ex x being Element of M st b2 = x -neighbour ); Lm1: for M being non empty Reflexive MetrStruct for x being Element of M holds x tolerates x ; theorem Th1: :: METRIC_2:1 for M being PseudoMetricSpace for x, y, z being Element of M st x tolerates y & y tolerates z holds x tolerates z proof let M be PseudoMetricSpace; ::_thesis: for x, y, z being Element of M st x tolerates y & y tolerates z holds x tolerates z let x, y, z be Element of M; ::_thesis: ( x tolerates y & y tolerates z implies x tolerates z ) assume ( x tolerates y & y tolerates z ) ; ::_thesis: x tolerates z then ( dist (x,y) = 0 & dist (y,z) = 0 ) by Def1; then dist (x,z) <= 0 + 0 by METRIC_1:4; then dist (x,z) = 0 by METRIC_1:5; hence x tolerates z by Def1; ::_thesis: verum end; theorem Th2: :: METRIC_2:2 for M being PseudoMetricSpace for x, y being Element of M holds ( y in x -neighbour iff y tolerates x ) proof let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M holds ( y in x -neighbour iff y tolerates x ) let x, y be Element of M; ::_thesis: ( y in x -neighbour iff y tolerates x ) hereby ::_thesis: ( y tolerates x implies y in x -neighbour ) assume y in x -neighbour ; ::_thesis: y tolerates x then ex q being Element of M st ( y = q & x tolerates q ) ; hence y tolerates x ; ::_thesis: verum end; assume y tolerates x ; ::_thesis: y in x -neighbour hence y in x -neighbour ; ::_thesis: verum end; theorem :: METRIC_2:3 for M being PseudoMetricSpace for 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; ::_thesis: for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds p tolerates q let x, p, q be Element of M; ::_thesis: ( p in x -neighbour & q in x -neighbour implies p tolerates q ) assume ( p in x -neighbour & q in x -neighbour ) ; ::_thesis: p tolerates q then ( p tolerates x & q tolerates x ) by Th2; hence p tolerates q by Th1; ::_thesis: verum end; theorem Th4: :: METRIC_2:4 for M being PseudoMetricSpace for x being Element of M holds x in x -neighbour proof let M be PseudoMetricSpace; ::_thesis: for x being Element of M holds x in x -neighbour let x be Element of M; ::_thesis: x in x -neighbour x tolerates x by Lm1; hence x in x -neighbour ; ::_thesis: verum end; theorem :: METRIC_2:5 for M being PseudoMetricSpace for x, y being Element of M st x in y -neighbour holds y in x -neighbour proof let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M st x in y -neighbour holds y in x -neighbour let x, y be Element of M; ::_thesis: ( x in y -neighbour implies y in x -neighbour ) assume x in y -neighbour ; ::_thesis: y in x -neighbour then x tolerates y by Th2; hence y in x -neighbour ; ::_thesis: verum end; theorem :: METRIC_2:6 for M being PseudoMetricSpace for p, x, y being Element of M st p in x -neighbour & x tolerates y holds p in y -neighbour proof let M be PseudoMetricSpace; ::_thesis: for p, x, y being Element of M st p in x -neighbour & x tolerates y holds p in y -neighbour let p, x, y be Element of M; ::_thesis: ( p in x -neighbour & x tolerates y implies p in y -neighbour ) assume that A1: p in x -neighbour and A2: x tolerates y ; ::_thesis: p in y -neighbour p tolerates x by A1, Th2; then p tolerates y by A2, Th1; hence p in y -neighbour ; ::_thesis: verum end; theorem Th7: :: METRIC_2:7 for M being PseudoMetricSpace for x, y being Element of M st y in x -neighbour holds x -neighbour = y -neighbour proof let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M st y in x -neighbour holds x -neighbour = y -neighbour let x, y be Element of M; ::_thesis: ( y in x -neighbour implies x -neighbour = y -neighbour ) assume A1: y in x -neighbour ; ::_thesis: x -neighbour = y -neighbour for p being Element of M st p in y -neighbour holds p in x -neighbour proof let p be Element of M; ::_thesis: ( p in y -neighbour implies p in x -neighbour ) assume p in y -neighbour ; ::_thesis: p in x -neighbour then A2: p tolerates y by Th2; y tolerates x by A1, Th2; then p tolerates x by A2, Th1; hence p in x -neighbour ; ::_thesis: verum end; then A3: y -neighbour c= x -neighbour by SUBSET_1:2; for p being Element of M st p in x -neighbour holds p in y -neighbour proof let p be Element of M; ::_thesis: ( p in x -neighbour implies p in y -neighbour ) assume p in x -neighbour ; ::_thesis: p in y -neighbour then A4: p tolerates x by Th2; x tolerates y by A1, Th2; then p tolerates y by A4, Th1; hence p in y -neighbour ; ::_thesis: verum end; then x -neighbour c= y -neighbour by SUBSET_1:2; hence x -neighbour = y -neighbour by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th8: :: METRIC_2:8 for M being PseudoMetricSpace for x, y being Element of M holds ( x -neighbour = y -neighbour iff x tolerates y ) proof let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M holds ( x -neighbour = y -neighbour iff x tolerates y ) let x, y be Element of M; ::_thesis: ( x -neighbour = y -neighbour iff x tolerates y ) hereby ::_thesis: ( x tolerates y implies x -neighbour = y -neighbour ) assume x -neighbour = y -neighbour ; ::_thesis: x tolerates y then x in y -neighbour by Th4; hence x tolerates y by Th2; ::_thesis: verum end; assume x tolerates y ; ::_thesis: x -neighbour = y -neighbour then x in y -neighbour ; hence x -neighbour = y -neighbour by Th7; ::_thesis: verum end; theorem :: METRIC_2:9 for M being PseudoMetricSpace for x, y being Element of M holds ( x -neighbour meets y -neighbour iff x tolerates y ) proof let M be PseudoMetricSpace; ::_thesis: for x, y being Element of M holds ( x -neighbour meets y -neighbour iff x tolerates y ) let x, y be Element of M; ::_thesis: ( x -neighbour meets y -neighbour iff x tolerates y ) hereby ::_thesis: ( x tolerates y implies x -neighbour meets y -neighbour ) assume x -neighbour meets y -neighbour ; ::_thesis: x tolerates y then consider p being set 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 = 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; ::_thesis: verum end; assume x tolerates y ; ::_thesis: x -neighbour meets y -neighbour then A4: x in y -neighbour ; x in x -neighbour by Th4; hence x -neighbour meets y -neighbour by A4, XBOOLE_0:3; ::_thesis: verum end; Lm2: for M being PseudoMetricSpace for V being equivalence_class of M holds V is non empty set proof let M be PseudoMetricSpace; ::_thesis: for V being equivalence_class of M holds V is non empty set let V be equivalence_class of M; ::_thesis: V is non empty set ex x being Element of M st V = x -neighbour by Def3; hence V is non empty set by Th4; ::_thesis: verum end; registration let M be PseudoMetricSpace; cluster -> non empty for equivalence_class of M; coherence for b1 being equivalence_class of M holds not b1 is empty by Lm2; end; theorem Th10: :: METRIC_2:10 for M being PseudoMetricSpace for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds dist (p,q) = 0 proof let M be PseudoMetricSpace; ::_thesis: for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds dist (p,q) = 0 let x, p, q be Element of M; ::_thesis: ( p in x -neighbour & q in x -neighbour implies dist (p,q) = 0 ) assume ( p in x -neighbour & q in x -neighbour ) ; ::_thesis: dist (p,q) = 0 then ( p tolerates x & q tolerates x ) by Th2; then p tolerates q by Th1; hence dist (p,q) = 0 by Def1; ::_thesis: verum end; theorem Th11: :: METRIC_2:11 for M being non empty Reflexive discerning MetrStruct for x, y being Element of M holds ( x tolerates y iff x = y ) proof let M be non empty Reflexive discerning MetrStruct ; ::_thesis: for x, y being Element of M holds ( x tolerates y iff x = y ) let x, y be Element of M; ::_thesis: ( x tolerates y iff x = y ) ( x tolerates y implies x = y ) proof assume x tolerates y ; ::_thesis: x = y then dist (x,y) = 0 by Def1; hence x = y by METRIC_1:2; ::_thesis: verum end; hence ( x tolerates y iff x = y ) ; ::_thesis: verum end; theorem Th12: :: METRIC_2:12 for M being non empty MetrSpace for x, y being Element of M holds ( y in x -neighbour iff y = x ) proof let M be non empty MetrSpace; ::_thesis: for x, y being Element of M holds ( y in x -neighbour iff y = x ) let x, y be Element of M; ::_thesis: ( y in x -neighbour iff y = x ) hereby ::_thesis: ( y = x implies y in x -neighbour ) assume y in x -neighbour ; ::_thesis: y = x then ex q being Element of M st ( y = q & x tolerates q ) ; hence y = x by Th11; ::_thesis: verum end; assume y = x ; ::_thesis: y in x -neighbour then x tolerates y by Th11; hence y in x -neighbour ; ::_thesis: verum end; theorem Th13: :: METRIC_2:13 for M being non empty MetrSpace for x being Element of M holds x -neighbour = {x} proof let M be non empty MetrSpace; ::_thesis: for x being Element of M holds x -neighbour = {x} let x be Element of M; ::_thesis: x -neighbour = {x} for p being Element of M st p in {x} holds p in x -neighbour proof let p be Element of M; ::_thesis: ( p in {x} implies p in x -neighbour ) assume p in {x} ; ::_thesis: p in x -neighbour then p = x by TARSKI:def_1; hence p in x -neighbour by Th12; ::_thesis: verum end; then A1: {x} c= x -neighbour by SUBSET_1:2; for p being Element of M st p in x -neighbour holds p in {x} proof let p be Element of M; ::_thesis: ( p in x -neighbour implies p in {x} ) assume p in x -neighbour ; ::_thesis: p in {x} then p = x by Th12; hence p in {x} by TARSKI:def_1; ::_thesis: verum end; then x -neighbour c= {x} by SUBSET_1:2; hence x -neighbour = {x} by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: METRIC_2:14 for M being non empty MetrSpace for 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; ::_thesis: for V being Subset of M holds ( V is equivalence_class of M iff ex x being Element of M st V = {x} ) let V be Subset of M; ::_thesis: ( V is equivalence_class of M iff ex x being Element of M st V = {x} ) 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 ; ::_thesis: ex x being Element of M st V = {x} then consider x being Element of M such that A2: V = x -neighbour by Def3; x -neighbour = {x} by Th13; hence ex x being Element of M st V = {x} by A2; ::_thesis: verum 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} ; ::_thesis: V is equivalence_class of M {x} = x -neighbour by Th13; hence V is equivalence_class of M by A3, Def3; ::_thesis: verum end; hence ( V is equivalence_class of M iff ex x being Element of M st V = {x} ) by A1; ::_thesis: verum end; definition let M be non empty MetrStruct ; funcM -neighbour -> set equals :: METRIC_2:def 4 { s where s is Subset of M : ex x being Element of M st x -neighbour = s } ; coherence { s where s is Subset of M : ex x being Element of M st x -neighbour = s } is set ; end; :: deftheorem defines -neighbour METRIC_2:def_4_:_ for M being non empty MetrStruct holds M -neighbour = { s where s is Subset of M : ex x being Element of M st x -neighbour = s } ; registration let M be non empty MetrStruct ; clusterM -neighbour -> non empty ; coherence not M -neighbour is empty proof set y = the Element of M; the Element of M -neighbour in { s where s is Subset of M : ex x being Element of M st x -neighbour = s } ; hence not M -neighbour is empty ; ::_thesis: verum end; end; theorem Th15: :: METRIC_2:15 for V being set for M being non empty MetrStruct holds ( V in M -neighbour iff ex x being Element of M st V = x -neighbour ) proof let V be set ; ::_thesis: for M being non empty MetrStruct holds ( V in M -neighbour iff ex x being Element of M st V = x -neighbour ) let M be non empty MetrStruct ; ::_thesis: ( V in M -neighbour iff ex x being Element of M st V = x -neighbour ) ( V in M -neighbour implies ex x being Element of M st V = x -neighbour ) proof assume V in M -neighbour ; ::_thesis: ex x being Element of M st V = x -neighbour then ex q being Subset of M st ( q = V & ex x being Element of M st q = x -neighbour ) ; hence ex x being Element of M st V = x -neighbour ; ::_thesis: verum end; hence ( V in M -neighbour iff ex x being Element of M st V = x -neighbour ) ; ::_thesis: verum end; theorem :: METRIC_2:16 for M being non empty MetrStruct for x being Element of M holds x -neighbour in M -neighbour ; theorem Th17: :: METRIC_2:17 for V being set for M being non empty MetrStruct holds ( V in M -neighbour iff V is equivalence_class of M ) proof let V be set ; ::_thesis: for M being non empty MetrStruct holds ( V in M -neighbour iff V is equivalence_class of M ) let M be non empty MetrStruct ; ::_thesis: ( V in M -neighbour iff V is equivalence_class of M ) A1: ( V is equivalence_class of M implies V in M -neighbour ) proof assume V is equivalence_class of M ; ::_thesis: V in M -neighbour then ex x being Element of M st V = x -neighbour by Def3; hence V in M -neighbour ; ::_thesis: verum end; ( V in M -neighbour implies V is equivalence_class of M ) proof assume V in M -neighbour ; ::_thesis: V is equivalence_class of M then ex x being Element of M st V = x -neighbour by Th15; hence V is equivalence_class of M by Def3; ::_thesis: verum end; hence ( V in M -neighbour iff V is equivalence_class of M ) by A1; ::_thesis: verum end; theorem :: METRIC_2:18 for M being non empty MetrSpace for x being Element of M holds {x} in M -neighbour proof let M be non empty MetrSpace; ::_thesis: for x being Element of M holds {x} in M -neighbour let x be Element of M; ::_thesis: {x} in M -neighbour x -neighbour = {x} by Th13; hence {x} in M -neighbour ; ::_thesis: verum end; theorem :: METRIC_2:19 for V being set for M being non empty MetrSpace holds ( V in M -neighbour iff ex x being Element of M st V = {x} ) proof let V be set ; ::_thesis: for M being non empty MetrSpace holds ( V in M -neighbour iff ex x being Element of M st V = {x} ) let M be non empty MetrSpace; ::_thesis: ( V in M -neighbour iff ex x being Element of M st V = {x} ) A1: ( V in M -neighbour implies ex x being Element of M st V = {x} ) proof assume V in M -neighbour ; ::_thesis: ex x being Element of M st V = {x} then consider x being Element of M such that A2: V = x -neighbour by Th15; x -neighbour = {x} by Th13; hence ex x being Element of M st V = {x} by A2; ::_thesis: verum 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} ; ::_thesis: V in M -neighbour x -neighbour = {x} by Th13; hence V in M -neighbour by A3; ::_thesis: verum end; hence ( V in M -neighbour iff ex x being Element of M st V = {x} ) by A1; ::_thesis: verum end; theorem Th20: :: METRIC_2:20 for M being PseudoMetricSpace for V, Q being Element of M -neighbour for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds dist (p1,q1) = dist (p2,q2) proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds dist (p1,q1) = dist (p2,q2) let V, Q be Element of M -neighbour ; ::_thesis: for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds dist (p1,q1) = dist (p2,q2) let p1, p2, q1, q2 be Element of M; ::_thesis: ( p1 in V & q1 in Q & p2 in V & q2 in Q implies dist (p1,q1) = dist (p2,q2) ) assume that A1: p1 in V and A2: q1 in Q and A3: p2 in V and A4: q2 in Q ; ::_thesis: dist (p1,q1) = dist (p2,q2) 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 dist (p1,q1) = dist (p2,q2) by A7, XXREAL_0:1; ::_thesis: verum end; definition let M be non empty MetrStruct ; let V, Q be Element of M -neighbour ; let v be Element of REAL ; predV,Q is_dst v means :Def5: :: METRIC_2:def 5 for p, q being Element of M st p in V & q in Q holds dist (p,q) = v; end; :: deftheorem Def5 defines is_dst METRIC_2:def_5_:_ for M being non empty MetrStruct for V, Q being Element of M -neighbour for v being Element of REAL holds ( V,Q is_dst v iff for p, q being Element of M st p in V & q in Q holds dist (p,q) = v ); theorem Th21: :: METRIC_2:21 for M being PseudoMetricSpace for V, Q being Element of M -neighbour for 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 ) ) proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour for 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 ) ) let V, Q be Element of M -neighbour ; ::_thesis: for 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 ) ) let v be Element of REAL ; ::_thesis: ( V,Q is_dst v iff ex p, q being Element of M st ( p in V & q in Q & dist (p,q) = v ) ) 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 ; ::_thesis: ex p, q being Element of M st ( p in V & q in Q & dist (p,q) = 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, Def5; hence ex p, q being Element of M st ( p in V & q in Q & dist (p,q) = v ) by A5, A3, Th4; ::_thesis: verum 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 ) proof assume ex p, q being Element of M st ( p in V & q in Q & dist (p,q) = v ) ; ::_thesis: V,Q is_dst v then for p1, q1 being Element of M st p1 in V & q1 in Q holds dist (p1,q1) = v by Th20; hence V,Q is_dst v by Def5; ::_thesis: verum end; hence ( V,Q is_dst v iff ex p, q being Element of M st ( p in V & q in Q & dist (p,q) = v ) ) by A1; ::_thesis: verum end; theorem Th22: :: METRIC_2:22 for M being PseudoMetricSpace for V, Q being Element of M -neighbour for v being Element of REAL st V,Q is_dst v holds Q,V is_dst v proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour for v being Element of REAL st V,Q is_dst v holds Q,V is_dst v let V, Q be Element of M -neighbour ; ::_thesis: for v being Element of REAL st V,Q is_dst v holds Q,V is_dst v let v be Element of REAL ; ::_thesis: ( V,Q is_dst v implies Q,V is_dst v ) assume V,Q is_dst v ; ::_thesis: Q,V is_dst v then for q, p being Element of M st q in Q & p in V holds dist (q,p) = v by Def5; hence Q,V is_dst v by Def5; ::_thesis: verum end; definition let M be non empty MetrStruct ; let 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 } ; coherence { v where v is Element of REAL : V,Q is_dst v } is Subset of REAL proof defpred S1[ Element of REAL ] means V,Q is_dst \$1; { v where v is Element of REAL : S1[v] } c= REAL from FRAENKEL:sch_10(); hence { v where v is Element of REAL : V,Q is_dst v } is Subset of REAL ; ::_thesis: verum end; end; :: deftheorem defines ev_eq_1 METRIC_2:def_6_:_ for M being non empty MetrStruct for V, Q being Element of M -neighbour holds ev_eq_1 (V,Q) = { v where v is Element of REAL : V,Q is_dst v } ; theorem :: METRIC_2:23 for M being PseudoMetricSpace for V, Q being Element of M -neighbour for v being Element of REAL holds ( v in ev_eq_1 (V,Q) iff V,Q is_dst v ) proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour for v being Element of REAL holds ( v in ev_eq_1 (V,Q) iff V,Q is_dst v ) let V, Q be Element of M -neighbour ; ::_thesis: for v being Element of REAL holds ( v in ev_eq_1 (V,Q) iff V,Q is_dst v ) let v be Element of REAL ; ::_thesis: ( v in ev_eq_1 (V,Q) iff V,Q is_dst v ) ( v in ev_eq_1 (V,Q) implies V,Q is_dst v ) proof assume v in ev_eq_1 (V,Q) ; ::_thesis: V,Q is_dst v then ex r being Element of REAL st ( r = v & V,Q is_dst r ) ; hence V,Q is_dst v ; ::_thesis: verum end; hence ( v in ev_eq_1 (V,Q) iff V,Q is_dst v ) ; ::_thesis: verum end; definition let M be non empty MetrStruct ; let 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 ) } ; coherence { 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 ) } is Subset of [:(M -neighbour),(M -neighbour):] proof defpred S1[ 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):] : S1[W] } c= [:(M -neighbour),(M -neighbour):] from FRAENKEL:sch_10(); hence { 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 ) } is Subset of [:(M -neighbour),(M -neighbour):] ; ::_thesis: verum end; end; :: deftheorem defines ev_eq_2 METRIC_2:def_7_:_ for M being non empty MetrStruct for v being Element of REAL holds ev_eq_2 (v,M) = { 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 ) } ; theorem :: METRIC_2:24 for M being PseudoMetricSpace for v being Element of REAL for 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; ::_thesis: for v being Element of REAL for 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 ) ) let v be Element of REAL ; ::_thesis: for 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 ) ) let W be Element of [:(M -neighbour),(M -neighbour):]; ::_thesis: ( 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 ) ) ( 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) ; ::_thesis: ex V, Q being Element of M -neighbour st ( W = [V,Q] & V,Q is_dst v ) 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 ex V, Q being Element of M -neighbour st ( W = [V,Q] & V,Q is_dst v ) ; ::_thesis: verum end; hence ( 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 ) ) ; ::_thesis: verum end; 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 } ; coherence { v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v } is Subset of REAL proof defpred S1[ 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 : S1[v] } c= REAL from FRAENKEL:sch_10(); hence { v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v } is Subset of REAL ; ::_thesis: verum end; end; :: deftheorem defines real_in_rel METRIC_2:def_8_:_ for M being non empty MetrStruct holds real_in_rel M = { v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v } ; theorem :: METRIC_2:25 for M being PseudoMetricSpace for 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; ::_thesis: for 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 ) let v be Element of REAL ; ::_thesis: ( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v ) ( 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 ; ::_thesis: ex V, Q being Element of M -neighbour st V,Q is_dst v then ex r being Element of REAL st ( v = r & ex V, Q being Element of M -neighbour st V,Q is_dst r ) ; hence ex V, Q being Element of M -neighbour st V,Q is_dst v ; ::_thesis: verum end; hence ( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v ) ; ::_thesis: verum end; 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 ex v being Element of REAL st V,Q is_dst v } ; coherence { V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of (M -neighbour) proof defpred S1[ Element of M -neighbour ] means ex Q being Element of M -neighbour ex v being Element of REAL st \$1,Q is_dst v; { V where V is Element of M -neighbour : S1[V] } c= M -neighbour from FRAENKEL:sch_10(); hence { V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of (M -neighbour) ; ::_thesis: verum end; end; :: deftheorem defines elem_in_rel_1 METRIC_2:def_9_:_ for M being non empty MetrStruct holds elem_in_rel_1 M = { V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ; theorem Th26: :: METRIC_2:26 for M being PseudoMetricSpace for V being Element of M -neighbour holds ( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) proof let M be PseudoMetricSpace; ::_thesis: for V being Element of M -neighbour holds ( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) let V be Element of M -neighbour ; ::_thesis: ( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ( V in elem_in_rel_1 M implies ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) proof assume V in elem_in_rel_1 M ; ::_thesis: ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v then ex S being Element of M -neighbour st ( S = V & ex Q being Element of M -neighbour ex v being Element of REAL st S,Q is_dst v ) ; hence ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ; ::_thesis: verum end; hence ( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ; ::_thesis: verum end; 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 ex v being Element of REAL st V,Q is_dst v } ; coherence { Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of (M -neighbour) proof defpred S1[ Element of M -neighbour ] means ex V being Element of M -neighbour ex v being Element of REAL st V,\$1 is_dst v; { Q where Q is Element of M -neighbour : S1[Q] } c= M -neighbour from FRAENKEL:sch_10(); hence { Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of (M -neighbour) ; ::_thesis: verum end; end; :: deftheorem defines elem_in_rel_2 METRIC_2:def_10_:_ for M being non empty MetrStruct holds elem_in_rel_2 M = { Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ; theorem Th27: :: METRIC_2:27 for M being PseudoMetricSpace for Q being Element of M -neighbour holds ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) proof let M be PseudoMetricSpace; ::_thesis: for Q being Element of M -neighbour holds ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) let Q be Element of M -neighbour ; ::_thesis: ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ( Q in elem_in_rel_2 M implies ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) proof assume Q in elem_in_rel_2 M ; ::_thesis: ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v then ex S being Element of M -neighbour st ( S = Q & ex V being Element of M -neighbour ex v being Element of REAL st V,S is_dst v ) ; hence ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ; ::_thesis: verum end; hence ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ; ::_thesis: verum end; 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 ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) } ; coherence { VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) } is Subset of [:(M -neighbour),(M -neighbour):] proof defpred S1[ Element of [:(M -neighbour),(M -neighbour):]] means ex V, Q being Element of M -neighbour ex v being Element of REAL st ( \$1 = [V,Q] & V,Q is_dst v ); { VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : S1[VQ] } c= [:(M -neighbour),(M -neighbour):] from FRAENKEL:sch_10(); hence { VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) } is Subset of [:(M -neighbour),(M -neighbour):] ; ::_thesis: verum end; end; :: deftheorem defines elem_in_rel METRIC_2:def_11_:_ for M being non empty MetrStruct holds elem_in_rel M = { VQ where VQ is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) } ; theorem :: METRIC_2:28 for M being PseudoMetricSpace for VQ being Element of [:(M -neighbour),(M -neighbour):] holds ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) ) proof let M be PseudoMetricSpace; ::_thesis: for VQ being Element of [:(M -neighbour),(M -neighbour):] holds ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) ) let VQ be Element of [:(M -neighbour),(M -neighbour):]; ::_thesis: ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) ) ( VQ in elem_in_rel M implies ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) ) proof assume VQ in elem_in_rel M ; ::_thesis: ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) then ex S being Element of [:(M -neighbour),(M -neighbour):] st ( VQ = S & ex V, Q being Element of M -neighbour ex v being Element of REAL st ( S = [V,Q] & V,Q is_dst v ) ) ; hence ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) ; ::_thesis: verum end; hence ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQ = [V,Q] & V,Q is_dst v ) ) ; ::_thesis: verum end; 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 ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) } ; coherence { VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) } is Subset of [:(M -neighbour),(M -neighbour),REAL:] proof defpred S1[ Element of [:(M -neighbour),(M -neighbour),REAL:]] means ex V, Q being Element of M -neighbour ex 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:] : S1[VQv] } c= [:(M -neighbour),(M -neighbour),REAL:] from FRAENKEL:sch_10(); hence { VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) } is Subset of [:(M -neighbour),(M -neighbour),REAL:] ; ::_thesis: verum end; end; :: deftheorem defines set_in_rel METRIC_2:def_12_:_ for M being non empty MetrStruct holds set_in_rel M = { VQv where VQv is Element of [:(M -neighbour),(M -neighbour),REAL:] : ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) } ; theorem Th29: :: METRIC_2:29 for M being PseudoMetricSpace for 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 ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) ) proof let M be PseudoMetricSpace; ::_thesis: for 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 ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) ) let VQv be Element of [:(M -neighbour),(M -neighbour),REAL:]; ::_thesis: ( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) ) ( VQv in set_in_rel M implies ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) ) proof assume VQv in set_in_rel M ; ::_thesis: ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) then ex S being Element of [:(M -neighbour),(M -neighbour),REAL:] st ( VQv = S & ex V, Q being Element of M -neighbour ex v being Element of REAL st ( S = [V,Q,v] & V,Q is_dst v ) ) ; hence ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) ; ::_thesis: verum end; hence ( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st ( VQv = [V,Q,v] & V,Q is_dst v ) ) ; ::_thesis: verum end; theorem :: METRIC_2:30 for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M proof let M be PseudoMetricSpace; ::_thesis: elem_in_rel_1 M = elem_in_rel_2 M for V being Element of M -neighbour st V in elem_in_rel_2 M holds V in elem_in_rel_1 M proof let V be Element of M -neighbour ; ::_thesis: ( V in elem_in_rel_2 M implies V in elem_in_rel_1 M ) assume V in elem_in_rel_2 M ; ::_thesis: V in elem_in_rel_1 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 V in elem_in_rel_1 M ; ::_thesis: verum 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 st V in elem_in_rel_1 M holds V in elem_in_rel_2 M proof let V be Element of M -neighbour ; ::_thesis: ( V in elem_in_rel_1 M implies V in elem_in_rel_2 M ) assume V in elem_in_rel_1 M ; ::_thesis: V in elem_in_rel_2 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 V in elem_in_rel_2 M ; ::_thesis: verum end; then elem_in_rel_1 M c= elem_in_rel_2 M by SUBSET_1:2; hence elem_in_rel_1 M = elem_in_rel_2 M by A2, XBOOLE_0:def_10; ::_thesis: verum end; 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):] proof let M be PseudoMetricSpace; ::_thesis: set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] for VQv being Element of [:(M -neighbour),(M -neighbour),REAL:] st VQv in set_in_rel M holds 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:]; ::_thesis: ( VQv in set_in_rel M implies VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] ) assume VQv in set_in_rel M ; ::_thesis: VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_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 VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by A1, A3, MCART_1:69; ::_thesis: verum end; hence set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by SUBSET_1:2; ::_thesis: verum end; theorem :: METRIC_2:32 for M being PseudoMetricSpace for V, Q being Element of M -neighbour for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds v1 = v2 proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds v1 = v2 let V, Q be Element of M -neighbour ; ::_thesis: for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds v1 = v2 let v1, v2 be Element of REAL ; ::_thesis: ( V,Q is_dst v1 & V,Q is_dst v2 implies v1 = v2 ) assume that A1: V,Q is_dst v1 and A2: V,Q is_dst v2 ; ::_thesis: v1 = 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, Def5; hence v1 = v2 by A2, A6, A5, Def5; ::_thesis: verum end; theorem Th33: :: METRIC_2:33 for M being PseudoMetricSpace for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v let V, Q be Element of M -neighbour ; ::_thesis: ex v being Element of REAL st V,Q is_dst v 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 ex v being Element of REAL st V,Q is_dst v ; ::_thesis: verum end; definition let M be PseudoMetricSpace; func nbourdist M -> Function of [:(M -neighbour),(M -neighbour):],REAL means :Def13: :: 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); existence ex b1 being Function of [:(M -neighbour),(M -neighbour):],REAL st for V, Q being Element of M -neighbour for p, q being Element of M st p in V & q in Q holds b1 . (V,Q) = dist (p,q) proof defpred S1[ Element of M -neighbour , Element of M -neighbour , Element of REAL ] means \$1,\$2 is_dst \$3; A1: for V, Q being Element of M -neighbour ex v being Element of REAL st S1[V,Q,v] by Th33; consider F being Function of [:(M -neighbour),(M -neighbour):],REAL such that A2: for V, Q being Element of M -neighbour holds S1[V,Q,F . (V,Q)] from BINOP_1:sch_3(A1); take F ; ::_thesis: for V, Q being Element of M -neighbour for p, q being Element of M st p in V & q in Q holds F . (V,Q) = dist (p,q) let V, Q be Element of M -neighbour ; ::_thesis: for p, q being Element of M st p in V & q in Q holds F . (V,Q) = dist (p,q) let p, q be Element of M; ::_thesis: ( p in V & q in Q implies F . (V,Q) = dist (p,q) ) assume A3: ( p in V & q in Q ) ; ::_thesis: F . (V,Q) = dist (p,q) V,Q is_dst F . (V,Q) by A2; hence F . (V,Q) = dist (p,q) by A3, Def5; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:(M -neighbour),(M -neighbour):],REAL st ( for V, Q being Element of M -neighbour for p, q being Element of M st p in V & q in Q holds b1 . (V,Q) = dist (p,q) ) & ( for V, Q being Element of M -neighbour for p, q being Element of M st p in V & q in Q holds b2 . (V,Q) = dist (p,q) ) holds b1 = b2 proof let F1, F2 be Function of [:(M -neighbour),(M -neighbour):],REAL; ::_thesis: ( ( 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) ) & ( 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) ) implies F1 = F2 ) assume that A4: 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 A5: 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) ; ::_thesis: F1 = F2 for V, Q being Element of M -neighbour holds F1 . (V,Q) = F2 . (V,Q) proof let V, Q be Element of M -neighbour ; ::_thesis: F1 . (V,Q) = F2 . (V,Q) consider p being Element of M such that A6: V = p -neighbour by Th15; consider q being Element of M such that A7: Q = q -neighbour by Th15; A8: q in Q by A7, Th4; A9: p in V by A6, Th4; then F1 . (V,Q) = dist (p,q) by A4, A8 .= F2 . (V,Q) by A5, A9, A8 ; hence F1 . (V,Q) = F2 . (V,Q) ; ::_thesis: verum end; hence F1 = F2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def13 defines nbourdist METRIC_2:def_13_:_ for M being PseudoMetricSpace for b2 being Function of [:(M -neighbour),(M -neighbour):],REAL holds ( b2 = nbourdist M iff for V, Q being Element of M -neighbour for p, q being Element of M st p in V & q in Q holds b2 . (V,Q) = dist (p,q) ); theorem Th34: :: METRIC_2:34 for M being PseudoMetricSpace for V, Q being Element of M -neighbour holds ( (nbourdist M) . (V,Q) = 0 iff V = Q ) proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour holds ( (nbourdist M) . (V,Q) = 0 iff V = Q ) let V, Q be Element of M -neighbour ; ::_thesis: ( (nbourdist M) . (V,Q) = 0 iff V = Q ) 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 ; ::_thesis: (nbourdist M) . (V,Q) = 0 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, Def1 ; hence (nbourdist M) . (V,Q) = 0 ; ::_thesis: verum end; ( (nbourdist M) . (V,Q) = 0 implies V = Q ) proof assume A6: (nbourdist M) . (V,Q) = 0 ; ::_thesis: V = Q 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 by Def1; hence V = Q by A7, A8, Th8; ::_thesis: verum end; hence ( (nbourdist M) . (V,Q) = 0 iff V = Q ) by A1; ::_thesis: verum end; theorem Th35: :: METRIC_2:35 for M being PseudoMetricSpace for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V) proof let M be PseudoMetricSpace; ::_thesis: for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V) let V, Q be Element of M -neighbour ; ::_thesis: (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V) 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 (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V) ; ::_thesis: verum end; theorem Th36: :: METRIC_2:36 for M being PseudoMetricSpace for 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; ::_thesis: for V, Q, W being Element of M -neighbour holds (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W)) let V, Q, W be Element of M -neighbour ; ::_thesis: (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W)) 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 (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W)) by A8, A6, METRIC_1:4; ::_thesis: verum end; definition let M be PseudoMetricSpace; func Eq_classMetricSpace M -> MetrSpace equals :: METRIC_2:def 14 MetrStruct(# (M -neighbour),(nbourdist M) #); coherence MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace proof set Z = MetrStruct(# (M -neighbour),(nbourdist M) #); now__::_thesis:_for_V,_Q,_W_being_Element_of_MetrStruct(#_(M_-neighbour),(nbourdist_M)_#)_holds_ (_(_dist_(V,Q)_=_0_implies_V_=_Q_)_&_(_V_=_Q_implies_dist_(V,Q)_=_0_)_&_dist_(V,Q)_=_dist_(Q,V)_&_dist_(V,W)_<=_(dist_(V,Q))_+_(dist_(Q,W))_) let V, Q, W be Element of MetrStruct(# (M -neighbour),(nbourdist M) #); ::_thesis: ( ( dist (V,Q) = 0 implies V = Q ) & ( V = Q implies dist (V,Q) = 0 ) & dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) ) 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; ::_thesis: ( dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) ) dist (Q,V) = (nbourdist M) . (Q9,V9) by METRIC_1:def_1; hence dist (V,Q) = dist (Q,V) by A1, Th35; ::_thesis: dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) ( 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; ::_thesis: verum end; hence MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace by METRIC_1:6; ::_thesis: verum end; end; :: deftheorem defines Eq_classMetricSpace METRIC_2:def_14_:_ for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour),(nbourdist M) #); registration let M be PseudoMetricSpace; cluster Eq_classMetricSpace M -> non empty strict ; coherence ( Eq_classMetricSpace M is strict & not Eq_classMetricSpace M is empty ) ; end;