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