notMem_nil

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#Cycle.notMem_nil

English

Every element is not a member of the empty cycle (nil).

Русский

Каждый элемент не является членом пустого цикла (nil).

LaTeX

$$$\forall a:\\ α,\\ a \notin (nil : Cycle α)$$$

Lean4

@[simp]
theorem notMem_nil (a : α) : a ∉ nil :=
  List.not_mem_nil

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

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

Разделы

Аффилиация

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