coe_antisymmetrization — Mathlib

English

The underlying function of the antisymmetrized map is precisely the quotient map of f with respect to the antisymmetry relation, i.e., the function part coincides with Quotient.map' f (liftFun_antisymmRel f).

Русский

Функциональная часть отображения антисимметризации совпадает с факторизацией по отношению антисимметрии: функция задаётся как Quotient.map' f (liftFun_antisymmRel f).

LaTeX

$$$\\text{coe}(f^{\\text{antisymmetrization}}) = \\ Quotient.map'\\ f\\ (liftFun_antisymmRel\; f)$$$

Lean4

@[simp]
theorem coe_antisymmetrization (f : α →o β) : ⇑f.antisymmetrization = Quotient.map' f (liftFun_antisymmRel f) :=
  rfl

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