next_mem

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#List.next_mem

English

If x is a member of a list l, then the next element after x in l is also a member of l.

Русский

Если x принадлежит списку l, то следующий за x элемент в списке l также принадлежит этому списку.

LaTeX

$$$\forall l:\\ List\ α\, \forall x:\\ α\, (h: x\in l)\quad l.next\ x\ h \in l$$$

Lean4

theorem next_mem (h : x ∈ l) : l.next x h ∈ l :=
  nextOr_mem (get_mem _ _)

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

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

Разделы

Аффилиация

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