sumArrowEquivProdArrow_apply — Mathlib

English

The ring isomorphism acts on a function x by the same underlying Equiv as the standard Equiv on sum arrows; i.e., its action coincides with the standard Equiv on the function space.

Русский

Изоморфизм действует на функцию x тем же базовым эквивалентом, что и стандартная эквивалентность для суммы функций.

LaTeX

$$$ sumArrowEquivProdArrow \alpha \beta R \; x = Equiv.sumArrowEquivProdArrow \alpha \beta R \; x $$$

Lean4

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

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