dropWhile_get_zero_not — Mathlib

English

If (l.dropWhile p).length > 0, then the first element of l.dropWhile p does not satisfy p.

Русский

Если длина l.dropWhile p больше нуля, тогда первый элемент l.dropWhile p не удовлетворяет p.

LaTeX

$$$|l.dropWhile(p)| > 0 \\Rightarrow p((l.dropWhile(p)).\\text{head}) = \\text{false}$$$

Lean4

theorem dropWhile_get_zero_not (l : List α) (hl : 0 < (l.dropWhile p).length) : ¬p ((l.dropWhile p).get ⟨0, hl⟩) := by
  induction l with
  | nil => cases hl
  | cons hd tl IH =>
    simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]

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