sumArrowEquivProdArrow_symm_apply_inr

English

The inverse of the sum-arrow to prod-arrow equivalence applied to a pair lands as the inverse Equiv on the right component.

Русский

Обратное отображение от суммарной к произведению даёт правый компонент как в случае обратного эквивалента.

LaTeX

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

Lean4

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

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