length_dropWhile_le — Mathlib

English

For any list l, the length of dropWhile p l is at most the length of l.

Русский

Для любого списка l длина dropWhile p l не превосходит длины l.

LaTeX

$$$\\mathrm{length}(\\mathrm{dropWhile}(p, l)) \\le \\mathrm{length}(l)$$$

Lean4

theorem length_dropWhile_le (l : List α) : (dropWhile p l).length ≤ l.length := by
  induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [dropWhile, length_cons]
    split
    · cutsat
    · simp

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