sumArrowEquivProdArrow_apply — Mathlib

English

The algebra equivalence sumArrowEquivProdArrow acts on x exactly as the underlying Equiv sumArrow equivalence: sumArrowEquivProdArrow α β R S x = Equiv.sumArrowEquivProdArrow α β S x.

Русский

Алгебраическое соответствие sumArrowEquivProdArrow действует на x точно как базовое эквивалентное отображение Equiv.sumArrowEquivProdArrow.

LaTeX

$$$$ \mathrm{sumArrowEquivProdArrow}(α, β, R, S)\;x = \mathrm{Equiv}.\mathrm{sumArrowEquivProdArrow}(α, β, S)\;x. $$$$

Lean4

@[simp low]
theorem sumArrowEquivProdArrow_apply (x : α ⊕ β → S) :
    sumArrowEquivProdArrow α β R S x = Equiv.sumArrowEquivProdArrow α β S x :=
  rfl

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