mathlib3 documentation

data.list.fin_range

Lists of elements of fin n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file develops some results on fin_range n.

source
@[simp]
theorem list.map_coe_fin_range (n : ℕ) :
list.map coe (list.fin_range n) = list.range n
source
theorem list.fin_range_succ_eq_map (n : ℕ) :
list.fin_range n.succ = 0 :: list.map fin.succ (list.fin_range n)
source
@[simp]
theorem list.map_nth_le {α : Type u} (l : list α) :
list.map (λ (n : fin l.length), l.nth_le ↑n _) (list.fin_range l.length) = l
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.of_fn_id (n : ℕ) :
list.of_fn id = list.fin_range n
source
theorem list.of_fn_eq_map {α : Type u_1} {n : ℕ} {f : fin n → α} :
list.of_fn f = list.map f (list.fin_range n)
source
theorem list.nodup_of_fn_of_injective {α : Type u_1} {n : ℕ} {f : fin n → α} (hf : function.injective f) :
(list.of_fn f).nodup
source
theorem list.nodup_of_fn {α : Type u_1} {n : ℕ} {f : fin n → α} :
(list.of_fn f).nodup ↔ function.injective f
source
theorem equiv.perm.map_fin_range_perm {n : ℕ} (σ : equiv.perm (fin n)) :
list.map ⇑σ (list.fin_range n) ~ list.fin_range n
source
theorem equiv.perm.of_fn_comp_perm {n : ℕ} {α : Type u} (σ : equiv.perm (fin n)) (f : fin n → α) :
list.of_fn (f ∘ ⇑σ) ~ list.of_fn f

The list obtained from a permutation of a tuple f is permutation equivalent to the list obtained from f.