dualAntisymmetrization_symm_apply

English

The dual of the antisymmetrization is naturally isomorphic to the antisymmetrization of the dual, via a canonical symmetry of the underlying relations.

Русский

Двойственная антисимметризация естественно изоморфна антисимметризации двойственного порядка.

LaTeX

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

Lean4

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

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