English
Given an injective map f: γ → β and a metric space structure on β, one can pull back the metric to γ via induced distance with the identification γ ≃ f(γ).
Русский
При инъективном отображении f: γ → β можно вытянуть метрическую структуру на γ через индукированное расстояние.
LaTeX
$$$ \text{MetricSpace.induced } f \ hf \text{ on } β$$$
Lean4
/-- Metric space structure pulled back by an injective function. Injectivity is necessary to
ensure that `dist x y = 0` only if `x = y`. -/
abbrev induced {γ β} (f : γ → β) (hf : Function.Injective f) (m : MetricSpace β) : MetricSpace γ :=
{ PseudoMetricSpace.induced f m.toPseudoMetricSpace with eq_of_dist_eq_zero := fun h => hf (dist_eq_zero.1 h) }
