sigmaAntidiagonalEquivProd_symm_apply_fst

English

The first coordinate of the inverse image equals the product a·b as established by the symmetry lemmas.

Русский

Первая компонента образа обратного изображения равна произведению a·b согласно симметрическим леммам.

LaTeX

$$$$ (sigmaAntidiagonalEquivProd.symm x).1 = x.1.1 \cdot x.2.1. $$$$

Lean4

theorem sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) :
    (sigmaAntidiagonalEquivProd.symm x).1 = x.1.1 * x.2.1 :=
  rfl

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