appendIsometry — Mathlib

English

There exists an isometry between (Fin m → α) × (Fin n → α) and Fin (m+n) → α.

Русский

Существует изометрия между (Fin m → α) × (Fin n → α) и Fin (m+n) → α.

LaTeX

$$$ (\Fin m \to α) \times (\Fin n \to α) \simeq_i (\Fin (m+n) \to α)$$$

Lean4

/-- The natural `IsometryEquiv` between `(Fin m → α) × (Fin n → α)` and `Fin (m + n) → α`.
`Fin.appendEquiv` as an `IsometryEquiv`. -/
@[simps!]
def _root_.Fin.appendIsometry (m n : ℕ) : (Fin m → α) × (Fin n → α) ≃ᵢ (Fin (m + n) → α)
    where
  toEquiv := Fin.appendEquiv _ _
  isometry_toFun _ _ := by simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]

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