antisymmetrization_apply — Mathlib

English

For an order-preserving map f: α →o β and an element a in Antisymmetrization α (≤), the antisymmetrized map applied to a equals the quotient of f applied to a, i.e., f.antisymmetrization a = Quotient.map' f (liftFun_antisymmRel f) a.

Русский

Для монотонного отображения f: α →o β и элемента a в антисимметризации α, отображение антисимметризации применяется к a как Quotient.map' f (liftFun_antisymmRel f) a.

LaTeX

$$$f.antisymmetrization(a) = \\ Quotient.map' f (liftFun_antisymmRel f)\\ a$$$

Lean4

theorem antisymmetrization_apply (f : α →o β) (a : Antisymmetrization α (· ≤ ·)) :
    f.antisymmetrization a = Quotient.map' f (liftFun_antisymmRel f) a :=
  rfl

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