Lists of elements of Fin n

This file develops some results on finRange n.

theorem List.finRange_eq_pmap_range (n : ℕ) : List.finRange n = List.pmap Fin.mk (List.range n) ⋯

@[simp]

theorem List.mem_finRange {n : ℕ} (a : Fin n) : a ∈ List.finRange n

theorem List.nodup_finRange (n : ℕ) : (List.finRange n).Nodup

@[simp]

theorem List.finRange_eq_nil {n : ℕ} : List.finRange n = [] ↔ n = 0

theorem List.pairwise_lt_finRange (n : ℕ) : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (List.finRange n)

theorem List.pairwise_le_finRange (n : ℕ) : List.Pairwise (fun (x1 x2 : Fin n) => x1 ≤ x2) (List.finRange n)

theorem List.get_finRange {n i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩

@[deprecated List.get_finRange]

theorem List.nthLe_finRange {n i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩

Alias of List.get_finRange.

@[simp]

theorem List.finRange_map_get {α : Type u} (l : List α) : List.map l.get (List.finRange l.length) = l

@[simp]

theorem List.indexOf_finRange {k : ℕ} (i : Fin k) : List.indexOf i (List.finRange k) = ↑i

@[simp]

theorem List.map_coe_finRange (n : ℕ) : List.map Fin.val (List.finRange n) = List.range n

theorem List.finRange_succ_eq_map (n : ℕ) : List.finRange n.succ = 0 :: List.map Fin.succ (List.finRange n)

theorem List.ofFn_eq_pmap {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.pmap (fun (i : ℕ) (hi : i < n) => f ⟨i, hi⟩) (List.range n) ⋯

theorem List.ofFn_id (n : ℕ) : List.ofFn id = List.finRange n

theorem List.ofFn_eq_map {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.map f (List.finRange n)

theorem List.nodup_ofFn_ofInjective {α : Type u} {n : ℕ} {f : Fin n → α} (hf : Function.Injective f) : (List.ofFn f).Nodup

theorem List.nodup_ofFn {α : Type u} {n : ℕ} {f : Fin n → α} : (List.ofFn f).Nodup ↔ Function.Injective f

theorem Equiv.Perm.map_finRange_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) : (List.map (⇑σ) (List.finRange n)).Perm (List.finRange n)

theorem Equiv.Perm.ofFn_comp_perm {n : ℕ} {α : Type u} (σ : Equiv.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.