It's a common theme in Mathlib to use some auxiliary typeclass to define the one we actually want to use. For example, to define PseudoMetricSpace
we use the typeclass Dist
given by the following:
@[ext]
class Dist (α : Type _) where
dist : α → α → ℝ
From what I understand this definition of Dist
doesn't come with any of the properties we'd like to be associated with a pseudometric. We then let PseudoMetricSpace
be an extension of Dist
where dist
has all the desired properties. My question is what was the point of starting with the typeclass Dist
? I.e., couldn't we just include the definition of dist
with type α → α → ℝ
inside PseudoMetricSpace
and take it along with any further extensions (say, to MetricSpace
)?
My intuition is that it probably helps establish a nice base for anything that needs a dist
function. Right or wrong, can you give an example of why this auxiliary Dist
is necessary/appealing?