instIsEmptySucc

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.instIsEmptySucc

English

If α is empty, then Sym α (n+1) is empty.

Русский

Если α пуст, то Sym α (n+1) пуст.

LaTeX

$$$\\operatorname{IsEmpty}(\\alpha) \\Rightarrow \\operatorname{IsEmpty}(\\mathrm{Sym}(\\alpha, n+1)).$$$

Lean4

instance (n : ℕ) [IsEmpty α] : IsEmpty (Sym α n.succ) :=
  ⟨fun s => by
    obtain ⟨a, -⟩ := exists_mem s
    exact isEmptyElim a⟩

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

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

Разделы

Аффилиация

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