prodEquiv_symm_apply_mk — Mathlib

English

The antisymmetrization of a product respects symmetry of the product; specifically, the projections to each factor correspond to the antisymmetrization of the respective factors.

Русский

Антисимметризация произведения сохраняет симметрию разложения на множители; проекции на каждый фактор соответствуют антисимметризации соответствующих факторов.

LaTeX

$$$\\text{prodEquiv}$ induces equality of projections: $\\pi_1(\\text{prodEquiv}(⟦a,b⟧)) = ⟦a⟧$, $\\pi_2(\\text{prodEquiv}(⟦a,b⟧)) = ⟦b⟧$$$

Lean4

@[simp]
theorem prodEquiv_symm_apply_mk {a b} : (prodEquiv α β).symm (⟦a⟧, ⟦b⟧) = ⟦(a, b)⟧ :=
  rfl

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