arrowProdEquivProdArrow — Mathlib

English

The type of functions to a product β × γ is equivalent to the type of pairs of functions α → β and α → γ.

Русский

Тип функций в произведении β × γ эквивалентен паре функций α → β и α → γ.

LaTeX

$$$((i : \alpha) \to (\beta i \times \gamma i)) \cong ((i : \alpha) \to \beta i) \times ((i : \alpha) \to \gamma i)$$$

Lean4

/-- The type of functions to a product `β × γ` is equivalent to the type of pairs of functions
`α → β` and `β → γ`. -/
@[simps]
def arrowProdEquivProdArrow (α : Type*) (β γ : α → Type*) : ((i : α) → β i × γ i) ≃ ((i : α) → β i) × ((i : α) → γ i)
    where
  toFun := fun f => (fun c => (f c).1, fun c => (f c).2)
  invFun := fun p c => (p.1 c, p.2 c)

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