sumArrowEquivProdArrow_apply_fst — Mathlib

English

The type of functions on a sum α ⊕ β is equivalent to the product of function types α → γ and β → γ.

Русский

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

LaTeX

$$$\text{sumArrowEquivProdArrow }(\alpha,\beta,\gamma) : (\alpha \oplus \beta \to \gamma) \cong (\alpha \to \gamma) \times (\beta \to \gamma)$$$

Lean4

@[simp]
theorem sumArrowEquivProdArrow_apply_fst {α β γ} (f : α ⊕ β → γ) (a : α) :
    (sumArrowEquivProdArrow α β γ f).1 a = f (inl a) :=
  rfl

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