sigmaAntidiagonalEquivProd_symm_apply_snd

English

The second coordinate of the inverse under sigmaAntidiagonalEquivProd is the pair (a,b) projected to its second coordinate.

Русский

Вторая компонента образа обратного отображения равна второй проекции пары (a,b).

LaTeX

$$$$ (sigmaAntidiagonalEquivProd.symm x).2 = (x.1.1, x.2.1). $$$$

Lean4

theorem sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) :
    (sigmaAntidiagonalEquivProd.symm x).2 = (x.1.1, x.2.1) :=
  rfl

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