find?_not_eq_head?_dropWhile — Mathlib

English

For any list l and predicate p, the equality find? (¬ p) l = (dropWhile p l).head? holds, i.e., the first element satisfying ¬ p x is the head of the list after dropping elements that satisfy p.

Русский

Для списка l и предиката p выполняется тождество: l.find? (¬ p) = (l.dropWhile p).head?, то есть первый элемент, удовлетворяющий ¬ p, совпадает с головой списка, полученного отбросив элементы, удовлетворяющие p.

LaTeX

$$$$ l.find? (\\lambda x. \\neg p(x)) = (l.dropWhile p).head? $$$$

Lean4

theorem find?_not_eq_head?_dropWhile : l.find? (fun x ↦ !(p x)) = (l.dropWhile p).head? :=
  by
  convert l.find?_eq_head?_dropWhile_not ?_
  simp

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