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

Equations

• e.dist = { dist := fun (x y : α) => dist (e x) (e y) }

@[reducible, inline]

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

Transfer a PseudoMetricSpace across an Equiv

Equations

• e.pseudometricSpace = PseudoMetricSpace.induced (⇑e) inst✝

@[reducible, inline]

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

Transfer a MetricSpace across an Equiv

Equations

• e.metricSpace = MetricSpace.induced ⇑e ⋯ inst✝