prodSumDistrib_symm_apply_left — Mathlib

English

Let a = (a1, a2) ∈ α × β. The inverse of the distributive equivalence between sums of pairs and a pair with a sum sends inl a to (a1, inl a2).

Русский

Пусть a = (a1, a2) ∈ α × β. Обратное отображение эквивалентности, переводящей сумму пару обратно, отправляет inl a на (a1, inl a2).

LaTeX

$$$\\\\big(\\\\mathrm{prodSumDistrib}\\\\ \\alpha\\\\ \\beta\\\\ \\gamma\\\\big)^{-1}(\\\\mathrm{inl}(a)) = (a_1, \\\\mathrm{inl}(a_2)).$$$

Lean4

@[simp]
theorem prodSumDistrib_symm_apply_left {α β γ} (a : α × β) : (prodSumDistrib α β γ).symm (inl a) = (a.1, inl a.2) :=
  rfl

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