isChain_cons_split — Mathlib

English

IsChain R (a :: (l1 ++ c :: l2)) holds iff IsChain R (a :: (l1 ++ [c])) and IsChain R (c :: l2).

Русский

IsChain R (a :: (l1 ++ c :: l2)) эквивалентно IsChain R (a :: (l1 ++ [c])) и IsChain R (c :: l2).

LaTeX

$$$IsChain\\;R\\;(a :: (l_1 ++ c :: l_2)) \\iff IsChain\\;R\\;(a :: (l_1 ++ [c])) \\land IsChain\\;R\\;(c :: l_2)$$$

Lean4

theorem isChain_cons_split {c : α} {l₁ l₂ : List α} :
    IsChain R (a :: (l₁ ++ c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [c])) ∧ IsChain R (c :: l₂) := by
  simp_rw [← cons_append, isChain_split (l₂ := l₂)]

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