Properties of List.enum

theorem List.forall_mem_zipIdx {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop} : (∀ x ∈ l.zipIdx n, p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], n + i)

theorem List.forall_mem_zipIdx' {α : Type u_1} {l : List α} {p : α × ℕ → Prop} : (∀ x ∈ l.zipIdx, p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], i)

Variant of forall_mem_zipIdx with the zipIdx argument specialized to 0.

theorem List.exists_mem_zipIdx {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop} : (∃ x ∈ l.zipIdx n, p x) ↔ ∃ (i : ℕ) (x : i < l.length), p (l[i], n + i)

theorem List.exists_mem_zipIdx' {α : Type u_1} {l : List α} {p : α × ℕ → Prop} : (∃ x ∈ l.zipIdx, p x) ↔ ∃ (i : ℕ) (x : i < l.length), p (l[i], i)

Variant of exists_mem_zipIdx with the zipIdx argument specialized to 0.