sumArrowEquivProdArrow_symm_apply_inl

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sumArrowEquivProdArrow_symm_apply_inl {α β γ} (f : α → γ) (g : β → γ) (a : α) :
    ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inl a) = f a :=
  rfl

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