isChain_append_cons_cons — Mathlib

English

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

Русский

IsChain R (l1, добавленный b :: c :: l2) эквивалентно IsChain R (l1 ++ [b]) и R b c и IsChain R (c :: l2).

LaTeX

$$$IsChain\\;R\\;(l_1 \\mathrm{\\;append\\;}(b :: c :: l_2)) \\iff IsChain\\;R\\;(l_1 \\mathrm{\\;append\\;}( [b] )) \\land R\\;b\\;c \\land IsChain\\;R\\;(c :: l_2)$$$

Lean4

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

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