antisymmetrization_apply_mk — Mathlib

English

There is an order-embedding of Antisymmetrization α (≤) into α, given by the out-relational embedding, i.e., the quotient out-rel embedding is injective and preserves order.

Русский

Существует вложение порядка антисимметризации α (≤) в α, задаваемое вложением Quotient.outRelEmbedding, сохраняющее и инъективное по отношению к порядку.

LaTeX

$$$\\text{ofAntisymmetrization} : Anti(α) \\hookrightarrow α$ preserves ≤ and is injective$$

Lean4

@[simp]
theorem antisymmetrization_apply_mk (f : α →o β) (a : α) :
    f.antisymmetrization (toAntisymmetrization _ a) = toAntisymmetrization _ (f a) :=
  @Quotient.map_mk _ _ (_root_.id _) (_root_.id _) f (liftFun_antisymmRel f) _

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