}.
notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
-interpretation "metric" 'delta2 a b = (metric _ _ a b).
+interpretation "metric" 'delta2 a b = (metric ? ? a b).
notation "\delta" non associative with precedence 80 for @{ 'delta }.
-interpretation "metric" 'delta = (metric _ _).
+interpretation "metric" 'delta = (metric ? ?).
lemma apart_of_metric_space: ∀R.metric_space R → apartness.
intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;