elim_nil

Mathlib.Data.List.Duplicate

URI: https://scilib.ai/kg/mathlib#List.Duplicate.elim_nil

English

No element can duplicate the empty list.

Русский

Никакой элемент не может дублировать пустой список.

LaTeX

$$$(x:\alpha)\in+ [] \Rightarrow \text{False}$$$

Lean4

theorem elim_nil (h : x ∈+ []) : False :=
  not_duplicate_nil x h

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

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

Разделы

Аффилиация

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