iff_mem

Mathlib.Data.List.Chain

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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