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} :

theorem List.exists_mem_zipIdx' {α : Type u_1} {l : List α} {p : α × ℕ → Prop} :

Variant of exists_mem_zipIdx with the zipIdx argument specialized to 0.

@[deprecated List.forall_mem_zipIdx (since := "2025-01-28")]

theorem List.forall_mem_enumFrom {α : 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)

Alias of List.forall_mem_zipIdx.

@[deprecated List.forall_mem_zipIdx' (since := "2025-01-28")]

theorem List.forall_mem_enum {α : Type u_1} {l : List α} {p : α × ℕ → Prop} :

(∀ (x : α × ℕ), x ∈ l.zipIdx → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], i)

Alias of List.forall_mem_zipIdx'.

Variant of forall_mem_zipIdx with the zipIdx argument specialized to 0.

@[deprecated List.exists_mem_zipIdx (since := "2025-01-28")]

theorem List.exists_mem_enumFrom {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop} :

Alias of List.exists_mem_zipIdx.

@[deprecated List.exists_mem_zipIdx' (since := "2025-01-28")]

theorem List.exists_mem_enum {α : Type u_1} {l : List α} {p : α × ℕ → Prop} :

Alias of List.exists_mem_zipIdx'.

Variant of exists_mem_zipIdx with the zipIdx argument specialized to 0.