lemma apart_of_metric_space: ∀R.metric_space R → apartness.
intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;
lemma apart_of_metric_space: ∀R.metric_space R → apartness.
intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;