English
For P : α → Prop, every element of the list of f satisfies P if and only if P holds for all f j with j : Fin n.
Русский
Для произвольного P: α → Prop, выполняется: все элементы List.ofFn f удовлетворяют P ⇔ ∀ j : Fin n, P (f j).
LaTeX
$$$ \\forall i \\in \\operatorname{List.ofFn} f\\, P(i) \\;\\Longleftrightarrow\\; \\forall j : \\mathrm{Fin}\, n,\\; P(f(j)) $$$
Lean4
@[simp]
theorem ofFn_getElem_eq_map {β : Type*} (l : List α) (f : α → β) :
ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := by
rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]
-- Note there is a now another `mem_ofFn` defined in Lean, with an existential on the RHS,
-- which is marked as a simp lemma.
