Documentation

Mathlib.Data.List.FinRange

Lists of elements of Fin n #

This file develops some results on finRange n.

source
theorem List.finRange_eq_pmap_range (n : ℕ) :
finRange n = pmap Fin.mk (range n) ⋯
source
@[simp]
theorem List.mem_finRange {n : ℕ} (a : Fin n) :
a ∈ finRange n
source
theorem List.nodup_finRange (n : ℕ) :
(finRange n).Nodup
source
@[simp]
theorem List.finRange_eq_nil {n : ℕ} :
finRange n = [] ↔ n = 0
source
theorem List.pairwise_lt_finRange (n : ℕ) :
Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (finRange n)
source
theorem List.pairwise_le_finRange (n : ℕ) :
Pairwise (fun (x1 x2 : Fin n) => x1 ≤ x2) (finRange n)
source
@[simp]
theorem List.count_finRange {n : ℕ} (a : Fin n) :
count a (finRange n) = 1
source
theorem List.get_finRange {n i : ℕ} (h : i < (finRange n).length) :
(finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩
source
@[simp]
theorem List.finRange_map_get {α : Type u} (l : List α) :
map l.get (finRange l.length) = l
source
@[simp]
theorem List.finRange_map_getElem {α : Type u} (l : List α) :
map (fun (x : Fin l.length) => l[↑x]) (finRange l.length) = l
source
@[simp]
theorem List.idxOf_finRange {k : ℕ} (i : Fin k) :
idxOf i (finRange k) = ↑i
source
@[deprecated List.idxOf_get (since := "2025-01-30")]
theorem List.indexOf_finRange {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : idxOf a l < l.length) :
l.get ⟨idxOf a l, h⟩ = a

Alias of List.idxOf_get.

source
@[simp]
theorem List.map_coe_finRange (n : ℕ) :
map Fin.val (finRange n) = range n
source
theorem List.finRange_succ_eq_map (n : ℕ) :
finRange n.succ = 0 :: map Fin.succ (finRange n)
source
theorem List.ofFn_eq_pmap {α : Type u} {n : ℕ} {f : Fin n → α} :
ofFn f = pmap (fun (i : ℕ) (hi : i < n) => f ⟨i, hi⟩) (range n) ⋯
source
theorem List.ofFn_id (n : ℕ) :
ofFn id = finRange n
source
theorem List.ofFn_eq_map {α : Type u} {n : ℕ} {f : Fin n → α} :
ofFn f = map f (finRange n)
source
theorem List.nodup_ofFn_ofInjective {α : Type u} {n : ℕ} {f : Fin n → α} (hf : Function.Injective f) :
(ofFn f).Nodup
source
theorem List.nodup_ofFn {α : Type u} {n : ℕ} {f : Fin n → α} :
(ofFn f).Nodup ↔ Function.Injective f
source
theorem Equiv.Perm.map_finRange_perm {n : ℕ} (σ : Perm (Fin n)) :
(List.map (⇑σ) (List.finRange n)).Perm (List.finRange n)
source
theorem Equiv.Perm.ofFn_comp_perm {n : ℕ} {α : Type u} (σ : Perm (Fin n)) (f : Fin n → α) :
(List.ofFn (f ∘ ⇑σ)).Perm (List.ofFn f)

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