isChain_cons'

Mathlib.Data.List.Chain

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

← MathLib Explorer

English

IsChain R (x :: l) is equivalent to (∀ y ∈ head? l, R x y) ∧ IsChain R l.

Русский

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

LaTeX

$$IsChain R (List.cons x l) ↔ (∀ y ∈ head? l, R x y) ∧ IsChain R l$$

Lean4

theorem isChain_cons' {x l} : IsChain R (x :: l) ↔ (∀ y ∈ head? l, R x y) ∧ IsChain R l :=
  ⟨fun h => ⟨h.rel_head?, h.tail⟩, fun ⟨h₁, h₂⟩ => h₂.cons' h₁⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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