isChain_cons_append_cons_cons — Mathlib

English

IsChain R (a :: (l1 ++ b :: c :: l2)) is equivalent to IsChain R (a :: (l1 ++ [b])) and R b c and IsChain R (c :: l2).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isChain_cons_append_cons_cons {a b c : α} {l₁ l₂ : List α} :
    IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂) := by
  rw [isChain_cons_split, isChain_cons_cons]

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