dropWhile_eq_nil_iff — Mathlib

English

dropWhile p l = [] iff every element of l satisfies p.

Русский

dropWhile p l = [] тогда и только тогда, когда каждый элемент l удовлетворяет p.

LaTeX

$$$\\mathrm{dropWhile}(p, l) = \\emptyset \\;\\iff\\; \\forall x \\in l, p(x)$$$

Lean4

@[simp]
theorem dropWhile_eq_nil_iff : dropWhile p l = [] ↔ ∀ x ∈ l, p x := by
  induction l with
  | nil => simp [dropWhile]
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

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