Transfer metric space structures across Equivs

In this file, we transfer a distance and (pseudo-)metric space structure across an equivalence.

@[reducible, inline]

abbrev Equiv.dist {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Dist β] : Dist α

Transfer a Dist across an Equiv

@[reducible, inline]

abbrev Equiv.pseudometricSpace {α : Type u_1} {β : Type u_2} [PseudoMetricSpace β] (e : α ≃ β) : PseudoMetricSpace α

Transfer a PseudoMetricSpace across an Equiv

@[reducible, inline]

abbrev Equiv.metricSpace {α : Type u_1} {β : Type u_2} [MetricSpace β] (e : α ≃ β) : MetricSpace α

Transfer a MetricSpace across an Equiv