nil_notMem_splitBy — Mathlib

English

The empty list never appears as a piece in the splitBy partition of any list l with respect to any r.

Русский

Пустой список никогда не образуется как часть разбиения splitBy для любого списка l и любого r.

LaTeX

$$$ \\text{nil} \\notin l.splitBy r $$$

Lean4

theorem nil_notMem_splitBy (r : α → α → Bool) (l : List α) : [] ∉ l.splitBy r :=
  match l with
  | nil => not_mem_nil
  | cons _ _ => nil_notMem_splitByLoop

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