isChain_of_mem_splitBy — Mathlib

English

If m is a member of l.splitBy with respect to r, then m is an r-chain; i.e., consecutive elements satisfy r.

Русский

Если m встречается в разбиении l.splitBy относительно r, то m образует r-цепочку: последовательные элементы удовлетворяют r.

LaTeX

$$$ m \\in l.splitBy r \\Rightarrow m.IsChain (\\lambda x y, r\\ x\\ y) $$$

Lean4

theorem isChain_of_mem_splitBy {r : α → α → Bool} {l : List α} (h : m ∈ l.splitBy r) : m.IsChain fun x y ↦ r x y := by
  cases l with
  | nil => cases h
  | cons a l =>
    apply isChain_of_mem_splitByLoop _ _ h
    · rintro _ ⟨⟩
    · exact isChain_nil

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