environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, FUNCT_1, ZFMISC_1, XBOOLE_0, PARTFUN1, SUBSET_1, REAL_1, RELAT_1, CARD_1, FUNCT_5, TARSKI, VALUED_0, ORDINAL1, XXREAL_0, ARYTM_3, RELAT_2, FUNCT_3, COMPLEX1, ARYTM_1, METRIC_1, FUNCOP_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCOP_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_5, VALUED_0, STRUCT_0;
definitions STRUCT_0, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_2, RELSET_1, RELAT_1, FUNCT_3, ABSVALUE, SUBSET_1, CARD_1, FUNCT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, SQUARE_1, FUNCOP_1, XREAL_0;
schemes FRAENKEL, BINOP_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0, FUNCT_2, PARTFUN1, RELSET_1, ORDINAL1, BINOP_2;
constructors HIDDEN, BINOP_1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, STRUCT_0, VALUED_1, FUNCT_5, PARTFUN1, RELSET_1, FUNCOP_1, NUMBERS;
requirements HIDDEN, BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
equalities BINOP_1, FUNCT_5, ORDINAL1;
expansions XBOOLE_0, BINOP_1;
Lm1:
0 in REAL
by XREAL_0:def 1;
Lm2:
op2 . (0,0) = 0
Lm3:
for x, y being Element of 1 holds
( op2 . (x,y) = 0 iff x = y )
Lm4:
for x, y being Element of 1 holds op2 . (x,y) = op2 . (y,x)
Lm5:
for x, y, z being Element of 1 holds op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z))
definition
let A be
set ;
existence
ex b1 being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) )
uniqueness
for b1, b2 being Function of [:A,A:],REAL st ( for x, y being Element of A holds
( b1 . (x,x) = 0 & ( x <> y implies b1 . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds
( b2 . (x,x) = 0 & ( x <> y implies b2 . (x,y) = 1 ) ) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of [:REAL,REAL:],REAL st
for x, y being Real holds b1 . (x,y) = |.(x - y).|
uniqueness
for b1, b2 being Function of [:REAL,REAL:],REAL st ( for x, y being Real holds b1 . (x,y) = |.(x - y).| ) & ( for x, y being Real holds b2 . (x,y) = |.(x - y).| ) holds
b1 = b2
end;
set M0 = MetrStruct(# 1,Empty^2-to-zero #);
:: let A,B be set, f be PartFunc of [:A,B:],REAL;
:: let a be Element of A;
:: let b be Element of B;
:: cluster f.(a,b) -> real;
:: coherence
:: proof
:: per cases;
:: suppose
:: [a,b] in dom f;
:: hence thesis by PARTFUN1:4;
:: end;
:: suppose
:: not [a,b] in dom f;
:: then f.(a,b) = 0 by FUNCT_1:def 2;
:: hence thesis;
:: end;
:: end;
:: end;