English
For any σ ∈ Perm(Fin n) and f: Fin n → α, the list of values of f after composing with σ is permutation-equivalent to that of f: ofFn (f ∘ σ) ~ ofFn f.
Русский
Для любой перестановки σ над Fin n и функции f: Fin n → α, последовательность значений f после композиции с σ эквивалентна перестановке списка ofFn f.
LaTeX
$$$$ \\operatorname{ofFn}(f \\circ \\sigma) \\sim \\operatorname{ofFn}(f). $$$$
Lean4
/-- The list obtained from a permutation of a tuple `f` is permutation equivalent to
the list obtained from `f`. -/
theorem ofFn_comp_perm {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α) : ofFn (f ∘ σ) ~ ofFn f :=
by
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
exact σ.map_finRange_perm.map f
