fact: Record is_MetricSpace {X : Type} (B: Q -> relation X) : Prop := { msp_refl: forall e, 0 <= e -> Reflexive (B e) ; msp_sym: forall e, Symmetric (B e) ; msp_triangle: forall e1 e2 a b c, B e1 a b -> B e2 b c -> B (e1 + e2) a c ; msp_closed: forall e a b, (forall d, 0 < d -> B (e + d) a b) -> B e a b ; msp_nonneg : forall e a b, B e a b -> 0 <= e ; msp_stable : forall e a b, (~~B e a b) -> B e a b }.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra