sumArrowIsometryEquivProdArrow — Mathlib

English

There is a natural isometry between maps on a sum α ⊕ β to γ and the product of maps α → γ and β → γ.

Русский

Существует естественная изометрия между отображениями на сумму α ⊕ β в γ и парой отображений α → γ, β → γ.

LaTeX

$$$ (α \oplus β) \to γ \quad\text{is isometric to}\quad (α \to γ) \times (β \to γ) $$$

Lean4

/-- The natural isometry `(α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)` between the type of maps on a sum of
fintypes `α ⊕ β` and the pairs of functions on the types `α` and `β`.
`Equiv.sumArrowEquivProdArrow` as an `IsometryEquiv`. -/
@[simps!]
def sumArrowIsometryEquivProdArrow [Fintype α] [Fintype β] : (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)
    where
  toEquiv := Equiv.sumArrowEquivProdArrow _ _ _
  isometry_toFun _ _ := by simp [Prod.edist_eq, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum]

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