English
Let α be a topological space and β a metric space. If f: α → β is an embedding, then α endowed with the metric induced by f from β makes f an isometry; equivalently, for all x,y ∈ α, d_β(f(x), f(y)) = d_α(x,y) where d_α(x,y) is the pullback metric d_β(f(x),f(y)).
Русский
Пусть α — топологическое пространство, β — метрическое пространство. Пусть f: α → β является вложением. Тогда α, снабжённое метрикой, индуцированной из β через f, образует изометрию f: α → β; то есть для всех x,y ∈ α выполняется d_β(f(x), f(y)) = d_α(x,y), причём d_α(x,y) = d_β(f(x), f(y)).
LaTeX
$$$ d_\beta(f(x), f(y)) = d_\alpha(x,y) \quad( x,y \in \alpha ), \; d_\alpha(x,y) := d_\beta(f(x), f(y)). $$$
Lean4
/-- An embedding from a topological space to a metric space is an isometry with respect to the
induced metric space structure on the source space. -/
theorem to_isometry {α β} [TopologicalSpace α] [MetricSpace β] {f : α → β} (h : IsEmbedding f) :
(letI := h.comapMetricSpace f;
Isometry f) :=
let _ := h.comapMetricSpace f
Isometry.of_dist_eq fun _ _ => rfl
