Membership in take and drop, positionally #
getElem?-indexed characterizations of membership in a prefix or suffix. Candidates
for Mathlib/Data/List/TakeDrop.lean.
theorem
List.mem_take_iff
{α : Type u_1}
{a : α}
{w : List α}
{k : ℕ}
:
a ∈ take k w ↔ ∃ (j : ℕ), j < k ∧ w[j]? = some a
theorem
List.mem_drop_iff
{α : Type u_1}
{a : α}
{w : List α}
{k : ℕ}
:
a ∈ drop k w ↔ ∃ (j : ℕ), j ≥ k ∧ w[j]? = some a