next_cons_cons_eq'

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#List.next_cons_cons_eq'

English

In a triple (y,z,l), if x∈y::z::l and x=y, then next(y::z::l) x h = z.

Русский

Для списка вида (y,z,l), если x принадлежит y::z::l и x=y, то next(y::z::l) x h = z.

LaTeX

$$$\\text{Given } y,z,l,\\ x∈y::z::l,\\ x=y:\\ next(y::z::l)\\ x\\ h = z$$$

Lean4

theorem next_cons_cons_eq' (y z : α) (h : x ∈ y :: z :: l) (hx : x = y) : next (y :: z :: l) x h = z := by
  rw [next, nextOr, if_pos hx]

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

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

Разделы

Аффилиация

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