instIsEmpty

Mathlib.Data.Sym.Sym2

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

English

If α is an empty type, then Sym2 α is empty as well.

Русский

Если α пустой тип, то и Sym2 α пуст.

LaTeX

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

Lean4

instance [IsEmpty α] : IsEmpty (Sym2 α) :=
  (equivSym α).isEmpty

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

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

Разделы

Аффилиация

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