Documentation

Mathlib.Data.List.Enum

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.

source
@[deprecated List.getElem?_enumFrom (since := "2024-08-15")]
theorem List.get?_enumFrom {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) :
(List.enumFrom n l).get? m = Option.map (fun (a : α) => (n + m, a)) (l.get? m)
source
@[deprecated List.get?_enumFrom (since := "2024-04-06")]
theorem List.enumFrom_get? {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) :
(List.enumFrom n l).get? m = Option.map (fun (a : α) => (n + m, a)) (l.get? m)

Alias of List.get?_enumFrom.

source
@[deprecated List.getElem?_enum (since := "2024-08-15")]
theorem List.get?_enum {α : Type u_1} (l : List α) (n : ℕ) :
l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)
source
@[deprecated List.get?_enum (since := "2024-04-06")]
theorem List.enum_get? {α : Type u_1} (l : List α) (n : ℕ) :
l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)

Alias of List.get?_enum.

source
@[deprecated List.getElem_enumFrom (since := "2024-08-15")]
theorem List.get_enumFrom {α : Type u_1} (l : List α) (n : ℕ) (i : Fin (List.enumFrom n l).length) :
(List.enumFrom n l).get i = (n + ↑i, l.get (Fin.cast ⋯ i))
source
@[deprecated List.getElem_enum (since := "2024-08-15")]
theorem List.get_enum {α : Type u_1} (l : List α) (i : Fin l.enum.length) :
l.enum.get i = (↑i, l.get (Fin.cast ⋯ i))
source
@[deprecated List.mk_add_mem_enumFrom_iff_getElem? (since := "2024-08-12")]
theorem List.mk_add_mem_enumFrom_iff_get? {α : Type u_1} {n i : ℕ} {x : α} {l : List α} :
(n + i, x) ∈ List.enumFrom n l ↔ l.get? i = some x
source
@[deprecated List.mk_mem_enumFrom_iff_le_and_getElem?_sub (since := "2024-08-12")]
theorem List.mk_mem_enumFrom_iff_le_and_get?_sub {α : Type u_1} {n i : ℕ} {x : α} {l : List α} :
(i, x) ∈ List.enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = some x
source
@[deprecated List.mk_mem_enum_iff_getElem? (since := "2024-08-15")]
theorem List.mk_mem_enum_iff_get? {α : Type u_1} {i : ℕ} {x : α} {l : List α} :
(i, x) ∈ l.enum ↔ l.get? i = some x
source
@[deprecated List.mem_enum_iff_getElem? (since := "2024-08-15")]
theorem List.mem_enum_iff_get? {α : Type u_1} {x : ℕ × α} {l : List α} :
x ∈ l.enum ↔ l.get? x.1 = some x.2
source
theorem List.forall_mem_enumFrom {α : Type u_1} {l : List α} {n : ℕ} {p : ℕ × α → Prop} :
(∀ (x : ℕ × α), x ∈ List.enumFrom n l → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (n + i, l[i])
source
theorem List.forall_mem_enum {α : Type u_1} {l : List α} {p : ℕ × α → Prop} :
(∀ (x : ℕ × α), x ∈ l.enum → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (i, l[i])
source
theorem List.exists_mem_enumFrom {α : Type u_1} {l : List α} {n : ℕ} {p : ℕ × α → Prop} :
(∃ (x : ℕ × α), x ∈ List.enumFrom n l ∧ p x) ↔ ∃ (i : ℕ), ∃ (x : i < l.length), p (n + i, l[i])
source
theorem List.exists_mem_enum {α : Type u_1} {l : List α} {p : ℕ × α → Prop} :
(∃ (x : ℕ × α), x ∈ l.enum ∧ p x) ↔ ∃ (i : ℕ), ∃ (x : i < l.length), p (i, l[i])