mathlib documentation

data.list.range

Ranges of naturals as lists #

This file shows basic results about list.iota, list.range, list.range' (all defined in data.list.defs) and defines list.fin_range. fin_range n is the list of elements of fin n. iota n = [1, ..., n] and range n = [0, ..., n - 1] are basic list constructions used for tactics. range' a b = [a, ..., a + b - 1] is there to help prove properties about them. Actual maths should use list.Ico instead.

@[simp]

theorem list.length_range' (s n : ℕ) :

(list.range' s n).length = n

@[simp]

theorem list.range'_eq_nil {s n : ℕ} :

list.range' s n = list.nil ↔ n = 0

@[simp]

theorem list.mem_range' {m s n : ℕ} :

m ∈ list.range' s n ↔ s ≤ m ∧ m < s + n

theorem list.map_add_range' (a s n : ℕ) :

list.map (has_add.add a) (list.range' s n) = list.range' (a + s) n

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

theorem list.chain_succ_range' (s n : ℕ) :

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

theorem list.chain_lt_range' (s n : ℕ) :

list.chain has_lt.lt s (list.range' (s + 1) n)

theorem list.pairwise_lt_range' (s n : ℕ) :

list.pairwise has_lt.lt (list.range' s n)

theorem list.nodup_range' (s n : ℕ) :

(list.range' s n).nodup

@[simp]

theorem list.range'_append (s m n : ℕ) :

list.range' s m ++ list.range' (s + m) n = list.range' s (n + m)

theorem list.range'_sublist_right {s m n : ℕ} :

list.range' s m <+ list.range' s n ↔ m ≤ n

theorem list.range'_subset_right {s m n : ℕ} :

list.range' s m ⊆ list.range' s n ↔ m ≤ n

theorem list.nth_range' (s : ℕ) {m n : ℕ} :

m < n → (list.range' s n).nth m = some (s + m)

@[simp]

theorem list.nth_le_range' {n m : ℕ} (i : ℕ) (H : i < (list.range' n m).length) :

(list.range' n m).nth_le i H = n + i

theorem list.range'_concat (s n : ℕ) :

list.range' s (n + 1) = list.range' s n ++ [s + n]

theorem list.range_core_range' (s n : ℕ) :

list.range_core s (list.range' s n) = list.range' 0 (n + s)

theorem list.range_eq_range' (n : ℕ) :

list.range n = list.range' 0 n

theorem list.range_succ_eq_map (n : ℕ) :

list.range (n + 1) = 0 :: list.map nat.succ (list.range n)

theorem list.range'_eq_map_range (s n : ℕ) :

list.range' s n = list.map (has_add.add s) (list.range n)

@[simp]

theorem list.length_range (n : ℕ) :

(list.range n).length = n

@[simp]

theorem list.range_eq_nil {n : ℕ} :

list.range n = list.nil ↔ n = 0

theorem list.pairwise_lt_range (n : ℕ) :

list.pairwise has_lt.lt (list.range n)

theorem list.nodup_range (n : ℕ) :

(list.range n).nodup

theorem list.range_sublist {m n : ℕ} :

list.range m <+ list.range n ↔ m ≤ n

theorem list.range_subset {m n : ℕ} :

list.range m ⊆ list.range n ↔ m ≤ n

@[simp]

theorem list.mem_range {m n : ℕ} :

m ∈ list.range n ↔ m < n

@[simp]

theorem list.not_mem_range_self {n : ℕ} :

n ∉ list.range n

@[simp]

theorem list.self_mem_range_succ (n : ℕ) :

n ∈ list.range (n + 1)

theorem list.nth_range {m n : ℕ} (h : m < n) :

(list.range n).nth m = some m

theorem list.range_succ (n : ℕ) :

list.range n.succ = list.range n ++ [n]

@[simp]

theorem list.range_zero :

list.range 0 = list.nil

theorem list.chain'_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :

list.chain' r (list.range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

theorem list.chain_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :

list.chain r a (list.range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

theorem list.range_add (a b : ℕ) :

list.range (a + b) = list.range a ++ list.map (λ (x : ℕ), a + x) (list.range b)

theorem list.iota_eq_reverse_range' (n : ℕ) :

list.iota n = (list.range' 1 n).reverse

@[simp]

theorem list.length_iota (n : ℕ) :

(list.iota n).length = n

theorem list.pairwise_gt_iota (n : ℕ) :

list.pairwise gt (list.iota n)

theorem list.nodup_iota (n : ℕ) :

(list.iota n).nodup

theorem list.mem_iota {m n : ℕ} :

m ∈ list.iota n ↔ 1 ≤ m ∧ m ≤ n

theorem list.reverse_range' (s n : ℕ) :

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

def list.fin_range (n : ℕ) :

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

Equations

list.fin_range n = list.pmap fin.mk (list.range n) _

@[simp]

theorem list.fin_range_zero :

list.fin_range 0 = list.nil

@[simp]

theorem list.mem_fin_range {n : ℕ} (a : fin n) :

a ∈ list.fin_range n

theorem list.nodup_fin_range (n : ℕ) :

(list.fin_range n).nodup

@[simp]

theorem list.length_fin_range (n : ℕ) :

(list.fin_range n).length = n

@[simp]

theorem list.fin_range_eq_nil {n : ℕ} :

list.fin_range n = list.nil ↔ n = 0

@[simp]

theorem list.map_coe_fin_range (n : ℕ) :

list.map coe (list.fin_range n) = list.range n

theorem list.fin_range_succ_eq_map (n : ℕ) :

list.fin_range n.succ = 0 :: list.map fin.succ (list.fin_range n)

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

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

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.

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.

@[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

@[simp]

theorem list.enum_map_fst {α : Type u} (l : list α) :

list.map prod.fst l.enum = list.range l.length

theorem list.enum_eq_zip_range {α : Type u} (l : list α) :

l.enum = (list.range l.length).zip l

@[simp]

theorem list.unzip_enum_eq_prod {α : Type u} (l : list α) :

l.enum.unzip = (list.range l.length, l)

theorem list.enum_from_eq_zip_range' {α : Type u} (l : list α) {n : ℕ} :

list.enum_from n l = (list.range' n l.length).zip l

@[simp]

theorem list.unzip_enum_from_eq_prod {α : Type u} (l : list α) {n : ℕ} :

(list.enum_from n l).unzip = (list.range' n l.length, l)

@[simp]

theorem list.nth_le_range {n : ℕ} (i : ℕ) (H : i < (list.range n).length) :

(list.range n).nth_le i H = i

@[simp]

theorem list.nth_le_fin_range {n i : ℕ} (h : i < (list.fin_range n).length) :

(list.fin_range n).nth_le i h = ⟨i, _⟩

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) _

theorem list.of_fn_id (n : ℕ) :

list.of_fn id = list.fin_range n

theorem list.of_fn_eq_map {α : Type u_1} {n : ℕ} {f : fin n → α} :

list.of_fn f = list.map f (list.fin_range n)

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

(list.of_fn f).nodup