to_isometry — Mathlib

English

A uniform embedding from a uniform space to a metric space yields an isometry for the induced metric on the source space.

Русский

Унифицированное вложение из равномерного пространства в метрическое пространство образует изометрию для индуцированной метрики в источнике.

LaTeX

$$$IsUniformEmbedding\to_isometry$$$

Lean4

/-- A uniform embedding from a uniform space to a metric space is an isometry with respect to the
induced metric space structure on the source space. -/
theorem to_isometry {α β} [UniformSpace α] [MetricSpace β] {f : α → β} (h : IsUniformEmbedding f) :
    (letI := h.comapMetricSpace f;
    Isometry f) :=
  let _ := h.comapMetricSpace f
  Isometry.of_dist_eq fun _ _ => rfl

Похожие утверждения