ne_nil

Mathlib.Data.List.Duplicate

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

English

If x is duplicated in a list l, then l is not empty.

Русский

Если для некоторого x существует дублирование в списке l, то этот список не пустой.

LaTeX

$$$\forall \alpha\, \forall l:\ List\ \alpha\, \forall x:\alpha,\; x \in+ l \Rightarrow l \neq []$$$

Lean4

theorem ne_nil (h : x ∈+ l) : l ≠ [] := fun H => (mem_nil_iff x).mp (H ▸ h.mem)

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

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

Разделы

Аффилиация

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