isometry_mk — Mathlib

English

The injection of a fiber into the disjoint union is an isometry.

Русский

Встраивание пространства в дизъюнктивное объединение является изометрией.

LaTeX

$$$\text{Isometry}(\Sigma.mk_i : E_i \to \Sigma_k E_k)$$$

Lean4

/-- The injection of a space in a disjoint union is an isometry -/
theorem isometry_mk (i : ι) : Isometry (Sigma.mk i : E i → Σ k, E k) :=
  Isometry.of_dist_eq fun x y => by simp

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