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