English
If m = n, then for any f: Fin m → α, the list created from f is equal to the list created from f composed with the cast from Fin n to Fin m; equivalently, ofFn f = ofFn (f ∘ Fin.cast h.symm).
Русский
Если m = n, то для любого f: Fin m → α список, получаемый из f, равен списку, получаемому из f после композиции с преобразованием Fin.cast h.symm.
LaTeX
$$$ \\operatorname{ofFn} f = \\operatorname{ofFn} (f \\circ \\operatorname{Fin.cast} (h^{-1})) $$$
Lean4
/-- Useful if `rw [← map_ofFn]` complains that `g ∘ f` is not the same as `fun i => g (f i)`. -/
theorem ofFn_comp' {β : Type*} {n : ℕ} (f : Fin n → α) (g : α → β) : ofFn (fun i => g (f i)) = map g (ofFn f) :=
(map_ofFn f g).symm
