English
The map a ↦ toAntisymmetrization α (≤) a is monotone with respect to the preorder structure, i.e., it preserves order relations.
Русский
Отображение a ↦ toAntisymmetrization α (≤) a монотонно по отношению к упорядочению.
LaTeX
$$$\\text{Monotone}(a \\mapsto \\text{toAntisymmetrization})$$$
Lean4
/-- `Antisymmetrization` and `orderDual` commute. -/
def dualAntisymmetrization : (Antisymmetrization α (· ≤ ·))ᵒᵈ ≃o Antisymmetrization αᵒᵈ (· ≤ ·)
where
toFun := (Quotient.map' id) fun _ _ => And.symm
invFun := (Quotient.map' id) fun _ _ => And.symm
left_inv a := Quotient.inductionOn' a fun a => by simp_rw [Quotient.map'_mk'', id]
right_inv a := Quotient.inductionOn' a fun a => by simp_rw [Quotient.map'_mk'', id]
map_rel_iff' := @fun a b => Quotient.inductionOn₂' a b fun _ _ => Iff.rfl
