dualAntisymmetrization_apply — Mathlib

English

Antisymmetrization commutes with taking order dual: the dual of Antisymmetrization α ≃ Antisymmetrization of αᵒᵈ, yielding an isomorphism of orders.

Русский

Антисимметризация коммутирует с операции двойственного порядка: двойственный порядок антисимметризации α эквивалентен антисимметризации αᵒᵈ.

LaTeX

$$$(\\text{Antisymmetrization}(α))^{\\mathrm{op}} \\cong_o \\text{Antisymmetrization}(α^{\\mathrm{op}})$$$

Lean4

@[simp]
theorem dualAntisymmetrization_apply (a : α) :
    OrderIso.dualAntisymmetrization _ (toDual <| toAntisymmetrization _ a) = toAntisymmetrization _ (toDual a) :=
  rfl

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