Properties of List.enum

Deprecation note

Many lemmas in this file have been replaced by theorems in Lean4, in terms of xs[i]? and xs[i] rather than get and get?.

The deprecated results here are unused in Mathlib. Any downstream users who can not easily adapt may remove the deprecations as needed.

theorem List.forall_mem_zipIdx {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop} : (∀ (x : α × ℕ), 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 : α × ℕ), 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 : α × ℕ), 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 : α × ℕ), 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.