Equiv.Perm.ofFn_comp_perm
theorem Equiv.Perm.ofFn_comp_perm :
∀ {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α), (List.ofFn (f ∘ ⇑σ)).Perm (List.ofFn f)
The theorem `Equiv.Perm.ofFn_comp_perm` states that for any natural number `n`, any type `α`, a permutation `σ` of finite set `Fin n`, and a function `f` from `Fin n` to `α`, the list obtained by applying the function `f` to the permuted elements of the finite set (`List.ofFn (f ∘ ⇑σ)`) is permutation equivalent to the list obtained by applying `f` to the elements of the finite set without permutation (`List.ofFn f`). In other words, permuting the indices first and then applying the function is the same as applying the function first and then permuting the list elements.
More concisely: For any natural number `n`, type `α`, permutation `σ` of `Fin n`, and function `f` from `Fin n` to `α`, `List.ofFn (f ∘ ⇑σ)` is permutation equivalent to `List.ofFn f`.
|
List.ofFn_eq_map
theorem List.ofFn_eq_map : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, List.ofFn f = List.map f (List.finRange n) := by
sorry
This theorem states that for any type `α` and natural number `n`, if `f` is a function that maps `Fin n` to `α`, then creating a list by applying `f` to each element from `0` to `n-1` (as done by `List.ofFn f`) is equivalent to first creating a list of all elements from `0` to `n-1` (as done by `List.finRange n`) and then mapping `f` over this list (i.e., `List.map f (List.finRange n)`). In other words, the theorem asserts the equality between two different ways of creating a list from a function that takes elements in `Fin n`.
More concisely: For any type `α` and natural number `n`, the function `List.map f (List.finRange n)` equals `List.ofFn f` when `f` maps `Fin n` to `α`.
|