Documentation

Mathlib.Data.List.Enum

Properties of List.enum #

@[simp]
theorem List.getElem?_enumFrom {α : Type u_1} (n : ) (l : List α) (m : ) :
(List.enumFrom n l)[m]? = Option.map (fun (a : α) => (n + m, a)) l[m]?
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)
@[deprecated List.get?_enumFrom]
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.

@[simp]
theorem List.getElem?_enum {α : Type u_1} (l : List α) (n : ) :
l.enum[n]? = Option.map (fun (a : α) => (n, a)) l[n]?
theorem List.get?_enum {α : Type u_1} (l : List α) (n : ) :
l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)
@[deprecated List.get?_enum]
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.

@[simp]
theorem List.enumFrom_map_snd {α : Type u_1} (n : ) (l : List α) :
List.map Prod.snd (List.enumFrom n l) = l
@[simp]
theorem List.enum_map_snd {α : Type u_1} (l : List α) :
List.map Prod.snd l.enum = l
@[simp]
theorem List.getElem_enumFrom {α : Type u_1} (l : List α) (n : ) (i : ) (h : i < (List.enumFrom n l).length) :
(List.enumFrom n l)[i] = (n + i, l[i])
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))
@[simp]
theorem List.getElem_enum {α : Type u_1} (l : List α) (i : ) (h : i < l.enum.length) :
l.enum[i] = (i, l[i])
theorem List.get_enum {α : Type u_1} (l : List α) (i : Fin l.enum.length) :
l.enum.get i = (i, l.get (Fin.cast i))
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
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
theorem List.mk_mem_enum_iff_get? {α : Type u_1} {i : } {x : α} {l : List α} :
(i, x) l.enum l.get? i = some x
theorem List.mem_enum_iff_get? {α : Type u_1} {x : × α} {l : List α} :
x l.enum l.get? x.1 = some x.2
theorem List.le_fst_of_mem_enumFrom {α : Type u_1} {x : × α} {n : } {l : List α} (h : x List.enumFrom n l) :
n x.1
theorem List.fst_lt_add_of_mem_enumFrom {α : Type u_1} {x : × α} {n : } {l : List α} (h : x List.enumFrom n l) :
x.1 < n + l.length
theorem List.fst_lt_of_mem_enum {α : Type u_1} {x : × α} {l : List α} (h : x l.enum) :
x.1 < l.length
theorem List.snd_mem_of_mem_enumFrom {α : Type u_1} {x : × α} {n : } {l : List α} (h : x List.enumFrom n l) :
x.2 l
theorem List.snd_mem_of_mem_enum {α : Type u_1} {x : × α} {l : List α} (h : x l.enum) :
x.2 l
theorem List.mem_enumFrom {α : Type u_1} {x : α} {i : } {j : } (xs : List α) (h : (i, x) List.enumFrom j xs) :
j i i < j + xs.length x xs
@[simp]
theorem List.enumFrom_singleton {α : Type u_1} (x : α) (n : ) :
List.enumFrom n [x] = [(n, x)]
@[simp]
theorem List.enum_singleton {α : Type u_1} (x : α) :
[x].enum = [(0, x)]
theorem List.enumFrom_append {α : Type u_1} (xs : List α) (ys : List α) (n : ) :
List.enumFrom n (xs ++ ys) = List.enumFrom n xs ++ List.enumFrom (n + xs.length) ys
theorem List.enum_append {α : Type u_1} (xs : List α) (ys : List α) :
(xs ++ ys).enum = xs.enum ++ List.enumFrom xs.length ys
theorem List.map_fst_add_enumFrom_eq_enumFrom {α : Type u_1} (l : List α) (n : ) (k : ) :
List.map (Prod.map (fun (x : ) => x + n) id) (List.enumFrom k l) = List.enumFrom (n + k) l
theorem List.map_fst_add_enum_eq_enumFrom {α : Type u_1} (l : List α) (n : ) :
List.map (Prod.map (fun (x : ) => x + n) id) l.enum = List.enumFrom n l
theorem List.enumFrom_cons' {α : Type u_1} (n : ) (x : α) (xs : List α) :
theorem List.enum_cons' {α : Type u_1} (x : α) (xs : List α) :
(x :: xs).enum = (0, x) :: List.map (Prod.map Nat.succ id) xs.enum
theorem List.enumFrom_map {α : Type u_1} {β : Type u_2} (n : ) (l : List α) (f : αβ) :
theorem List.enum_map {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) :
(List.map f l).enum = List.map (Prod.map id f) l.enum
@[simp]
theorem List.enumFrom_eq_nil {α : Type u_1} {n : } {l : List α} :
List.enumFrom n l = [] l = []
@[simp]
theorem List.enum_eq_nil {α : Type u_1} {l : List α} :
l.enum = [] l = []