List.find? under a stronger predicate #
The first element of a list satisfying q is also the first satisfying any predicate p that
it satisfies and that implies q on the list, since an earlier element satisfying p would
satisfy q. [UPSTREAM] candidate for Mathlib/Data/List/Find.lean.
Main results #
List.find?_eq_some_of_imp:find?stays put under a stronger predicate the found element satisfies.
theorem
List.find?_eq_some_of_imp
{α : Type u_1}
{p q : α → Bool}
{l : List α}
{a : α}
(hq : find? q l = some a)
(hp : p a = true)
(h : ∀ (x : α), x ∈ l → p x = true → q x = true)
:
find? p l = some a
The first element satisfying q is the first satisfying any stronger predicate it
satisfies.