sym_bijective

Mathlib.Algebra.Symmetrized

URI: https://scilib.ai/kg/mathlib#SymAlg.sym_bijective

English

The map EquivLike.toFunLike.coe SymAlg.sym is bijective.

Русский

Отображение равносильности, соответствующее SymAlg.sym, биективно.

LaTeX

$$$\text{Bijective}(\mathrm{coe}(\mathrm{SymAlg}.sym))$$$

Lean4

theorem sym_bijective : Bijective (sym : α → αˢʸᵐ) :=
  sym.bijective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru