English
For any n, α and β, if f: Fin n → α and g: α → β, then applying g to the list created from f is the same as creating a list from the composition g ∘ f; i.e., List.map g (List.ofFn f) = List.ofFn (g ∘ f).
Русский
Для любого n, α, β, если f: Fin n → α и g: α → β, то применение g к списку, полученному из f, равно списку, полученному из композиции g ∘ f; то есть List.map g (List.ofFn f) = List.ofFn (g ∘ f).
LaTeX
$$$ \\operatorname{List.map} g (\\operatorname{List.ofFn} f) = \\operatorname{List.ofFn} (g \\circ f) $$$
Lean4
@[simp]
theorem map_ofFn {β : Type*} {n : ℕ} (f : Fin n → α) (g : α → β) : map g (ofFn f) = ofFn (g ∘ f) :=
ext_get (by simp) fun i h h' => by simp
