toInductiveLimit_isometry — Mathlib

English

The map toInductiveLimit I n is an isometry (alternative formulation).

Русский

Отображение toInductiveLimit I n — изометрия (альтернативная формулировка).

LaTeX

$$$\text{Isometry}(\text{toInductiveLimit}(I,n))$$$

Lean4

/-- The map `toInductiveLimit n` mapping `X n` to the inductive limit is an isometry. -/
theorem toInductiveLimit_isometry (I : ∀ n, Isometry (f n)) (n : ℕ) : Isometry (toInductiveLimit I n) :=
  Isometry.of_dist_eq fun x y => by
    change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
    rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self, leRecOn_self]

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