iff_mem_mem_tail

Mathlib.Data.List.Chain

URI: https://scilib.ai/kg/mathlib#List.IsChain.iff_mem_mem_tail

English

IsChain R l is equivalent to IsChain (x ∈ l ∧ y ∈ l.tail ∧ R x y) l.

Русский

IsChain R l эквивалентно IsChain (x ∈ l ∧ y ∈ l.tail ∧ R x y) l.

LaTeX

$$$IsChain\\;R\\;l \\iff IsChain\\; (\\lambda x,y. x \\in l \\land y \\in l.tail \\land R\\,x\\,y)\\;l$$$

Lean4

theorem iff_mem_mem_tail {l : List α} : IsChain R l ↔ IsChain (fun x y => x ∈ l ∧ y ∈ l.tail ∧ R x y) l :=
  IsChain.iff_of_mem_tail_imp <| by grind

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

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

Разделы

Аффилиация

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