instSubsingleton

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.instSubsingleton

English

If α is a subsingleton, then the symmetric square Sym2 α is also a subsingleton.

Русский

Если α является подсуператом, то Sym2 α тоже подсупертан.

LaTeX

$$$[\\mathrm{Subsingleton}(\\alpha)] \\Rightarrow \\mathrm{Subsingleton}(\\mathrm{Sym}^2(\\alpha))$$$

Lean4

instance [Subsingleton α] : Subsingleton (Sym2 α) :=
  (equivSym α).injective.subsingleton

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

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

Разделы

Аффилиация

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