sumArrowEquivProdArrow_symm_apply_inr

English

Let α, β, γ be types and f: α → γ, g: β → γ. Under the natural bijection between (α ⊕ β) → γ and (α → γ) × (β → γ), the inverse maps (f, g) to a function h with h(inr b) = g(b) for all b ∈ β.

Русский

Пусть α, β, γ — множества; пусть f: α → γ, g: β → γ. Существует естественная биекция между функциями (α ⊕ β) → γ и парами функций (α → γ) × (β → γ). Обратная биекция отправляет пару (f, g) в функцию h, такую что h(inr b) = g(b) для всех b ∈ β.

LaTeX

$$$\big( \text{sumArrowEquivProdArrow}_{\alpha\beta\gamma} \big)^{-1} (f,g) \big( \mathrm{inr}(b) \big) = g(b).$$$

Lean4

@[simp]
theorem sumArrowEquivProdArrow_symm_apply_inr {α β γ} (f : α → γ) (g : β → γ) (b : β) :
    ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inr b) = g b :=
  rfl

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