isChain_split — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isChain_split {c : α} {l₁ l₂ : List α} :
    IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂) := by
  induction l₁ using twoStepInduction generalizing l₂ with grind

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