takeWhile_eq_self_iff — Mathlib

English

takeWhile p l = [] iff the first element of l does not satisfy p (when l is nonempty).

Русский

takeWhile p l = [] эквив. тому, что первый элемент l не удовлетворяет p (если l непуст).

LaTeX

$$$\\mathrm{takeWhile}(p, l) = \\emptyset \\;\\iff\\; \\forall hl: 0 < |l|, \\; \\lnot p(l[0])$$$

Lean4

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

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