ms_carr :> Type;
metric: ms_carr → ms_carr → R;
mpositive: ∀a,b:ms_carr. 0 ≤ metric a b;
mreflexive: ∀a. metric a a ≈ 0;
msymmetric: ∀a,b. metric a b ≈ metric b a;
mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
ms_carr :> Type;
metric: ms_carr → ms_carr → R;
mpositive: ∀a,b:ms_carr. 0 ≤ metric a b;
mreflexive: ∀a. metric a a ≈ 0;
msymmetric: ∀a,b. metric a b ≈ metric b a;
mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b