environ
vocabularies HIDDEN, NUMBERS, METRIC_1, SUBSET_1, REAL_1, XXREAL_0, TARSKI, ARYTM_3, XBOOLE_0, PRE_TOPC, SETFAM_1, ZFMISC_1, COMPTS_1, STRUCT_0, RCOMP_1, FINSET_1, FINSEQ_1, RELAT_1, NAT_1, CARD_1, FUNCT_1, CARD_5, ARYTM_1, PCOMPS_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, TOPS_2, SETFAM_1, DOMAIN_1, STRUCT_0, FINSET_1, COMPTS_1, PRE_TOPC, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1, NAT_1, METRIC_1;
definitions TARSKI;
theorems PRE_TOPC, TOPS_1, TOPS_2, NAT_1, FINSET_1, SUBSET_1, SETFAM_1, TARSKI, FINSEQ_1, ZFMISC_1, FUNCT_1, FUNCT_2, METRIC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0;
schemes SUBSET_1, FUNCT_2, NAT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, FINSEQ_1, PRE_TOPC, RELAT_1, ORDINAL1, BINOP_2, VALUED_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, REAL_1, SQUARE_1, NAT_1, MEMBERED, FINSEQ_1, TOPS_2, COMPTS_1, METRIC_1, RELSET_1, BINOP_1, BINOP_2, VALUED_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, COMPTS_1, SUBSET_1, RELAT_1;
expansions TARSKI, COMPTS_1;
definition
let D be
set ;
let f be
Function of
[:D,D:],
REAL;
pred f is_metric_of D means
for
a,
b,
c being
Element of
D holds
( (
f . (
a,
b)
= 0 implies
a = b ) & (
a = b implies
f . (
a,
b)
= 0 ) &
f . (
a,
b)
= f . (
b,
a) &
f . (
a,
c)
<= (f . (a,b)) + (f . (b,c)) );
end;
::
deftheorem defines
is_metric_of PCOMPS_1:def 6 :
for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) );