Mathlib.Data.List.FinRange

List.finRange_eq_pmap_range theorem

(n : ℕ) : finRange n = (range n).pmap Fin.mk (by simp)

Full source

theorem finRange_eq_pmap_range (n : ℕ) : finRange n = (range n).pmap Fin.mk (by simp) := by
  apply List.ext_getElem <;> simp [finRange]

Equality of `finRange` and Partial Map of Range via `Fin.mk`

Informal description

For any natural number $n$, the list `finRange n` is equal to the partial map of the range `[0, n)` using the constructor `Fin.mk`, with the proof obligation `by simp`.

List.mem_finRange theorem

{n : ℕ} (a : Fin n) : a ∈ finRange n

Full source

@[simp]
theorem mem_finRange {n : ℕ} (a : Fin n) : a ∈ finRange n := by
  rw [finRange_eq_pmap_range]
  exact mem_pmap.2
    ⟨a.1, mem_range.2 a.2, by
      cases a
      rfl⟩

Membership in `finRange` List for Finite Types

Informal description

For any natural number $n$ and any element $a$ of the finite type $\mathrm{Fin}\,n$, the element $a$ belongs to the list $\mathrm{finRange}\,n$.

List.nodup_finRange theorem

(n : ℕ) : (finRange n).Nodup

Full source

theorem nodup_finRange (n : ℕ) : (finRange n).Nodup := by
  rw [finRange_eq_pmap_range]
  exact (Pairwise.pmap nodup_range _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩

No Duplicates in `finRange` List

Informal description

For any natural number $n$, the list `finRange n` has no duplicate elements.

List.finRange_eq_nil theorem

{n : ℕ} : finRange n = [] ↔ n = 0

Full source

@[simp]
theorem finRange_eq_nil {n : ℕ} : finRangefinRange n = [] ↔ n = 0 := by
  rw [← length_eq_zero_iff, length_finRange]

Empty `finRange` List Condition: `finRange n = [] ↔ n = 0`

Informal description

For any natural number $n$, the list `finRange n` is empty if and only if $n = 0$.

List.pairwise_lt_finRange theorem

(n : ℕ) : Pairwise (· < ·) (finRange n)

Full source

theorem pairwise_lt_finRange (n : ℕ) : Pairwise (· < ·) (finRange n) := by
  rw [finRange_eq_pmap_range]
  exact List.pairwise_lt_range.pmap (by simp) (by simp)

Pairwise Strict Ordering of `finRange n` Elements by $<$

Informal description

For any natural number $n$, the list `finRange n` is pairwise ordered with respect to the strict less-than relation $<$. That is, for any two distinct elements $i$ and $j$ in `finRange n$, we have $i < j$ or $j < i$.

List.pairwise_le_finRange theorem

(n : ℕ) : Pairwise (· ≤ ·) (finRange n)

Full source

theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n) := by
  rw [finRange_eq_pmap_range]
  exact List.pairwise_le_range.pmap (by simp) (by simp)

Pairwise Ordering of `finRange n` Elements by $\leq$

Informal description

For any natural number $n$, the list `finRange n` is pairwise ordered with respect to the less-than-or-equal relation $\leq$. That is, for any two distinct elements $i$ and $j$ in `finRange n`, we have $i \leq j$ or $j \leq i$.

List.count_finRange theorem

{n : ℕ} (a : Fin n) : count a (finRange n) = 1

Full source

@[simp]
lemma count_finRange {n : ℕ} (a : Fin n) : count a (finRange n) = 1 := by
  simp [count_eq_of_nodup (nodup_finRange n)]

Count of Elements in $\mathrm{finRange}\ n$ is One

Informal description

For any natural number $n$ and any element $a$ in $\mathrm{Fin}\ n$, the count of $a$ in the list $\mathrm{finRange}\ n$ is equal to $1$.

List.get_finRange theorem

{n : ℕ} {i : ℕ} (h) : (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange (n := n) ▸ h⟩

Full source

theorem get_finRange {n : ℕ} {i : ℕ} (h) :
    (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange (n := n) ▸ h⟩ := by
  simp

Element Retrieval in `finRange` List

Informal description

For any natural number $n$ and index $i \in \mathbb{N}$ with proof $h$ that $i$ is a valid index for the list `finRange n`, the element at position $\langle i, h \rangle$ in `finRange n` is equal to the pair $\langle i, h' \rangle$, where $h'$ is the proof that $i$ is a valid index derived from the length of `finRange n$.

List.finRange_map_get theorem

(l : List α) : (finRange l.length).map l.get = l

Full source

@[simp]
theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
  List.ext_get (by simp) (by simp)

List Reconstruction via `finRange` and `get`

Informal description

For any list `l` of elements of type `α`, the list obtained by mapping the `get` function over the `finRange` of `l`'s length is equal to `l` itself. In other words, if we create a list of indices `finRange l.length` and then retrieve the corresponding elements from `l` using these indices, we recover the original list `l`.

List.finRange_map_getElem theorem

(l : List α) : (finRange l.length).map (l[·.1]) = l

Full source

@[simp]
theorem finRange_map_getElem (l : List α) : (finRange l.length).map (l[·.1]) = l :=
  finRange_map_get l

List Reconstruction via Index Mapping: $\text{map } (l[\cdot]) \text{ finRange}(l.\text{length}) = l$

Informal description

For any list $l$ of elements of type $\alpha$, the list obtained by mapping the element access function $l[\cdot]$ over the list of indices $\text{finRange}(l.\text{length})$ is equal to $l$ itself. In other words, if we create a list of indices $\text{finRange}(l.\text{length})$ and then retrieve the corresponding elements from $l$ using these indices, we recover the original list $l$.

List.idxOf_finRange theorem

{k : ℕ} (i : Fin k) : (finRange k).idxOf i = i

Full source

@[simp] theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by
  simpa using idxOf_getElem (nodup_finRange k) i

Index of Element in `finRange` List Equals the Element Itself

Informal description

For any natural number $k$ and any element $i$ of the finite type $\text{Fin }k$, the index of $i$ in the list $\text{finRange }k$ is equal to $i$ itself.

List.map_coe_finRange theorem

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

Full source

@[simp]
theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by
  apply List.ext_getElem <;> simp

Mapping Fin values to naturals yields the range list: `map Fin.val (finRange n) = range n`

Informal description

For any natural number $n$, the list obtained by mapping the underlying natural number value of each element in the list `finRange n` (which is a list of all elements of `Fin n`) is equal to the list `range n` (which is the list of natural numbers from $0$ to $n-1$). In other words, if we take the list `finRange n` (of type `List (Fin n)`), cast it to `List (Fin n)`, and then map each element to its underlying natural number value (via `Fin.val`), the result is the list `range n`.

List.finRange_succ_eq_map theorem

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

Full source

theorem finRange_succ_eq_map (n : ℕ) : finRange n.succ = 0 :: (finRange n).map Fin.succ := by
  apply map_injective_iff.mpr Fin.val_injective
  rw [map_cons, map_coe_finRange, range_succ_eq_map, Fin.val_zero, ← map_coe_finRange, map_map,
    map_map]
  simp only [Function.comp_def, Fin.val_succ]

Recursive Construction of `finRange` via Successor Mapping

Informal description

For any natural number $n$, the list `finRange (n + 1)` enumerating all elements of `Fin (n + 1)` is equal to the list obtained by prepending `0` to the list `finRange n` where each element is incremented by `Fin.succ`. In other words, $\operatorname{finRange}(n+1) = 0 :: \operatorname{map}\, \operatorname{Fin.succ}\, (\operatorname{finRange}\, n)$.

List.ofFn_eq_pmap theorem

{n} {f : Fin n → α} : ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) fun _ => mem_range.1

Full source

theorem ofFn_eq_pmap {n} {f : Fin n → α} :
    ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) fun _ => mem_range.1 := by
  rw [pmap_eq_map_attach]
  exact ext_getElem (by simp) fun i hi1 hi2 => by simp [List.getElem_ofFn hi1]

Equality of `ofFn` and Partial Map over Range

Informal description

For any natural number $n$ and any function $f \colon \mathrm{Fin}\,n \to \alpha$, the list obtained by applying $f$ to all elements of $\mathrm{Fin}\,n$ (via `ofFn f`) is equal to the partial map (`pmap`) of $f$ over the indices in the range $[0, n)$, where each index is coerced to a $\mathrm{Fin}\,n$ element with the appropriate proof.

List.ofFn_id theorem

(n) : ofFn id = finRange n

Full source

theorem ofFn_id (n) : ofFn id = finRange n :=
  rfl

Identity Function Generates $\operatorname{finRange}$ List

Informal description

For any natural number $n$, the list obtained by applying the identity function to all elements of $\operatorname{Fin} n$ is equal to the list $\operatorname{finRange} n$, which enumerates all elements of $\operatorname{Fin} n$ in order.

List.ofFn_eq_map theorem

{n} {f : Fin n → α} : ofFn f = (finRange n).map f

Full source

theorem ofFn_eq_map {n} {f : Fin n → α} : ofFn f = (finRange n).map f := by
  rw [← ofFn_id, map_ofFn, Function.comp_id]

Equality of `ofFn` and Mapping over `finRange`

Informal description

For any natural number $n$ and any function $f \colon \operatorname{Fin} n \to \alpha$, the list obtained by applying $f$ to all elements of $\operatorname{Fin} n$ (via $\operatorname{ofFn} f$) is equal to the list obtained by mapping $f$ over the list $\operatorname{finRange} n$, i.e., $\operatorname{ofFn} f = \operatorname{map} f (\operatorname{finRange} n)$.

List.nodup_ofFn_ofInjective theorem

{n} {f : Fin n → α} (hf : Function.Injective f) : Nodup (ofFn f)

Full source

theorem nodup_ofFn_ofInjective {n} {f : Fin n → α} (hf : Function.Injective f) :
    Nodup (ofFn f) := by
  rw [ofFn_eq_pmap]
  exact nodup_range.pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

Injective Functions Yield Duplicate-Free Lists on $\mathrm{Fin}\,n$

Informal description

For any natural number $n$ and any injective function $f \colon \mathrm{Fin}\,n \to \alpha$, the list obtained by applying $f$ to all elements of $\mathrm{Fin}\,n$ (via `ofFn f`) has no duplicate elements.

List.nodup_ofFn theorem

{n} {f : Fin n → α} : Nodup (ofFn f) ↔ Function.Injective f

Full source

theorem nodup_ofFn {n} {f : Fin n → α} : NodupNodup (ofFn f) ↔ Function.Injective f := by
  refine ⟨?_, nodup_ofFn_ofInjective⟩
  refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f
  · intro _
    exact Function.injective_of_subsingleton _
  · intro h
    rw [Fin.cons_injective_iff]
    simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
    exact h.imp_right ih

Duplicate-Free List from $\operatorname{Fin} n$ iff Function is Injective

Informal description

For any natural number $n$ and any function $f \colon \operatorname{Fin} n \to \alpha$, the list obtained by applying $f$ to all elements of $\operatorname{Fin} n$ (via $\operatorname{ofFn} f$) has no duplicate elements if and only if $f$ is injective.

Equiv.Perm.map_finRange_perm theorem

{n : ℕ} (σ : Equiv.Perm (Fin n)) : map σ (finRange n) ~ finRange n

Full source

theorem Equiv.Perm.map_finRange_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    mapmap σ (finRange n) ~ finRange n := by
  rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
  simpa [mem_map, mem_finRange] using σ.surjective

Permutation of `finRange` under a Bijection

Informal description

For any natural number $n$ and any permutation $\sigma$ of the finite set $\mathrm{Fin}\,n$, the list obtained by applying $\sigma$ to each element of the list $\mathrm{finRange}\,n$ is a permutation of $\mathrm{finRange}\,n$.

Equiv.Perm.ofFn_comp_perm theorem

{n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α) : ofFn (f ∘ σ) ~ ofFn f

Full source

/-- The list obtained from a permutation of a tuple `f` is permutation equivalent to
the list obtained from `f`. -/
theorem Equiv.Perm.ofFn_comp_perm {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α) :
    ofFnofFn (f ∘ σ) ~ ofFn f := by
  rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
  exact σ.map_finRange_perm.map f

Permutation of List under Function Composition with Permutation

Informal description

For any natural number $n$, any type $\alpha$, and any permutation $\sigma$ of the finite set $\{0, \dots, n-1\}$, the list obtained by applying the composition $f \circ \sigma$ to all elements of $\{0, \dots, n-1\}$ is a permutation of the list obtained by applying $f$ directly to $\{0, \dots, n-1\}$.