dropWhile_idempotent — Mathlib

English

Applying dropWhile with the same predicate twice is the same as applying it once: dropWhile p (dropWhile p l) = dropWhile p l.

Русский

Повторное применение dropWhile с одинаковым предикатом не меняет результат: dropWhile p (dropWhile p l) = dropWhile p l.

LaTeX

$$$$ \mathrm{dropWhile}(p, \mathrm{dropWhile}(p, l)) = \mathrm{dropWhile}(p, l). $$$$

Lean4

theorem dropWhile_idempotent : dropWhile p (dropWhile p l) = dropWhile p l :=
  by
  simp only [dropWhile_eq_self_iff]
  exact fun h => dropWhile_get_zero_not p l h

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