English
The construction Antisymmetrization α (≤) → Antisymmetrization β (≤) sends an order-preserving map f: α →o β to a corresponding order-preserving map between antisymmetrizations, defined by [a] ↦ [f(a)].
Русский
Конструкция антисимметризации α → Antisymmetrization β отправляет сохранное монотонное отображение f: α →o β в соответствующее монотонное отображение между антисимметризациями, задаваемое $[a] \mapsto [f(a)]$.
LaTeX
$$$f^{\\#}([a]) = [f(a)]$ for all a$$
Lean4
/-- Turns an order homomorphism from `α` to `β` into one from `Antisymmetrization α` to
`Antisymmetrization β`. `Antisymmetrization` is actually a functor. See `Preorder_to_PartialOrder`.
-/
protected def antisymmetrization (f : α →o β) : Antisymmetrization α (· ≤ ·) →o Antisymmetrization β (· ≤ ·) :=
⟨Quotient.map' f <| liftFun_antisymmRel f, fun a b => Quotient.inductionOn₂' a b <| f.mono⟩
