agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

Published 20 hours ago • verified publisher icon agda

ℚ forms a metric space over itself with the usual distance function

Open Taneb opened this issue 3 years ago • 0 comments

We should add Function.Metric.Rational.IsMetric (λ p q → ∣ p - q ∣) to Data.Rational.Properties and maybe to Data.Rational.Unnormalised.Properties too

Taneb avatar Sep 20 '22 06:09 Taneb