toAntisymmetrization_mono — Mathlib

English

The map sending an order homomorphism f: α →o β to its antisymmetrized version f.antisymmetrization is a monotone operator with respect to the induced orders.

Русский

Отображение, отправляющее остойчивое отображение f: α →o β в его антисимметризированную версию, сохраняет монотонность относительно индуцированных порядков.

LaTeX

$$$\\text{Monotone}(\\text{toAntisymmetrization})$$$

Lean4

@[mono]
theorem toAntisymmetrization_mono : Monotone (toAntisymmetrization (α := α) (· ≤ ·)) := fun _ _ => id

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