environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions ;
theorems TARSKI, BINOP_1, METRIC_1, SUBSET_1, MCART_1, XBOOLE_0, XXREAL_0, XREAL_0;
schemes FRAENKEL, BINOP_1;
registrations SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, METRIC_1, ORDINAL1;
constructors HIDDEN, DOMAIN_1, XXREAL_0, REAL_1, MEMBERED, METRIC_1, BINOP_1;
requirements HIDDEN, REAL, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities ;
expansions ;
Lm1:
for M being non empty Reflexive MetrStruct
for x being Element of M holds x tolerates x
;
Lm2:
for M being PseudoMetricSpace
for V being equivalence_class of M holds V is non empty set
definition
let M be
PseudoMetricSpace;
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)
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
end;