mathlib documentation

data.list.range

source
@[simp]
theorem list.length_range' (s n : ℕ) :
(list.range' s n).length = n

source
@[simp]
theorem list.mem_range' {m s n : ℕ} :
m ∈ list.range' s n ↔ s ≤ m ∧ m < s + n

source
theorem list.map_add_range' (a s n : ℕ) :
list.map (has_add.add a) (list.range' s n) = list.range' (a + s) n

source
theorem list.map_sub_range' (a s n : ℕ) (h : a ≤ s) :
list.map (λ (x : ℕ), x - a) (list.range' s n) = list.range' (s - a) n

source
theorem list.chain_succ_range' (s n : ℕ) :
list.chain (λ (a b : ℕ), b = a.succ) s (list.range' (s + 1) n)

source
theorem list.chain_lt_range' (s n : ℕ) :
list.chain has_lt.lt s (list.range' (s + 1) n)

source
theorem list.pairwise_lt_range' (s n : ℕ) :
list.pairwise has_lt.lt (list.range' s n)

source
theorem list.nodup_range' (s n : ℕ) :
(list.range' s n).nodup

source
@[simp]
theorem list.range'_append (s m n : ℕ) :
list.range' s m ++ list.range' (s + m) n = list.range' s (n + m)

source
theorem list.range'_sublist_right {s m n : ℕ} :
list.range' s m <+ list.range' s n ↔ m ≤ n

source
theorem list.range'_subset_right {s m n : ℕ} :
list.range' s m ⊆ list.range' s n ↔ m ≤ n

source
theorem list.nth_range' (s : ℕ) {m n : ℕ} (a : m < n) :
(list.range' s n).nth m = some (s + m)

source
theorem list.range'_concat (s n : ℕ) :
list.range' s (n + 1) = list.range' s n ++ [s + n]

source
theorem list.range_core_range' (s n : ℕ) :
list.range_core s (list.range' s n) = list.range' 0 (n + s)

source
theorem list.range_eq_range' (n : ℕ) :
list.range n = list.range' 0 n

source
theorem list.range_succ_eq_map (n : ℕ) :
list.range (n + 1) = 0 :: list.map nat.succ (list.range n)

source
theorem list.range'_eq_map_range (s n : ℕ) :
list.range' s n = list.map (has_add.add s) (list.range n)

source
@[simp]
theorem list.length_range (n : ℕ) :
(list.range n).length = n

source
theorem list.pairwise_lt_range (n : ℕ) :
list.pairwise has_lt.lt (list.range n)

source
theorem list.nodup_range (n : ℕ) :
(list.range n).nodup

source
theorem list.range_sublist {m n : ℕ} :
list.range m <+ list.range n ↔ m ≤ n

source
theorem list.range_subset {m n : ℕ} :
list.range m ⊆ list.range n ↔ m ≤ n

source
@[simp]
theorem list.mem_range {m n : ℕ} :
m ∈ list.range n ↔ m < n

source
@[simp]
theorem list.not_mem_range_self {n : ℕ} :
n ∉ list.range n

source
@[simp]
theorem list.self_mem_range_succ (n : ℕ) :
n ∈ list.range (n + 1)

source
theorem list.nth_range {m n : ℕ} (h : m < n) :
(list.range n).nth m = some m

source
theorem list.range_concat (n : ℕ) :
list.range n.succ = list.range n ++ [n]

source
theorem list.iota_eq_reverse_range' (n : ℕ) :
list.iota n = (list.range' 1 n).reverse

source
@[simp]
theorem list.length_iota (n : ℕ) :
(list.iota n).length = n

source
theorem list.pairwise_gt_iota (n : ℕ) :
list.pairwise gt (list.iota n)

source
theorem list.nodup_iota (n : ℕ) :
(list.iota n).nodup

source
theorem list.mem_iota {m n : ℕ} :
m ∈ list.iota n ↔ 1 ≤ m ∧ m ≤ n

source
theorem list.reverse_range' (s n : ℕ) :
(list.range' s n).reverse = list.map (λ (i : ℕ), s + n - 1 - i) (list.range n)

source
def list.fin_range (n : ℕ) :
list (fin n)

All elements of fin n, from 0 to n-1.

Equations
source
@[simp]
theorem list.mem_fin_range {n : ℕ} (a : fin n) :
a ∈ list.fin_range n

source
theorem list.nodup_fin_range (n : ℕ) :
(list.fin_range n).nodup

source
@[simp]
theorem list.length_fin_range (n : ℕ) :
(list.fin_range n).length = n

source
theorem list.prod_range_succ {α : Type u} [monoid α] (f : ℕ → α) (n : ℕ) :
(list.map f (list.range n.succ)).prod = ((list.map f (list.range n)).prod) * f n

source
theorem list.sum_range_succ {α : Type u} [add_monoid α] (f : ℕ → α) (n : ℕ) :
(list.map f (list.range n.succ)).sum = (list.map f (list.range n)).sum + f n

source
theorem list.prod_range_succ' {α : Type u} [monoid α] (f : ℕ → α) (n : ℕ) :
(list.map f (list.range n.succ)).prod = (f 0) * (list.map (λ (i : ℕ), f i.succ) (list.range n)).prod

A variant of prod_range_succ which pulls off the first term in the product rather than the last.

source
theorem list.sum_range_succ' {α : Type u} [add_monoid α] (f : ℕ → α) (n : ℕ) :
(list.map f (list.range n.succ)).sum = f 0 + (list.map (λ (i : ℕ), f i.succ) (list.range n)).sum

A variant of sum_range_succ which pulls off the first term in the sum rather than the last.

source
@[simp]
theorem list.enum_from_map_fst {α : Type u} (n : ℕ) (l : list α) :
list.map prod.fst (list.enum_from n l) = list.range' n l.length

source
@[simp]
theorem list.enum_map_fst {α : Type u} (l : list α) :
list.map prod.fst l.enum = list.range l.length

source
@[simp]
theorem list.nth_le_range {n : ℕ} (i : ℕ) (H : i < (list.range n).length) :
(list.range n).nth_le i H = i

source
theorem list.of_fn_eq_pmap {α : Type u_1} {n : ℕ} {f : fin n → α} :
list.of_fn f = list.pmap (λ (i : ℕ) (hi : i < n), f ⟨i, hi⟩) (list.range n) _

source
theorem list.nodup_of_fn {α : Type u_1} {n : ℕ} {f : fin n → α} (hf : function.injective f) :
(list.of_fn f).nodup