English
For any n and f: Fin n → α, the list of values given by ofFn f equals the pmap form over range n: ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) mem_range.1.
Русский
Для любого n и f: Fin n → α, список значений, полученный как OfFn f, эквивалентен форме pmap над range n: ofFn f = pmap (λ i hi, f ⟨i, hi⟩) (range n) mem_range.1.
LaTeX
$$$$ \\text{ofFn}(f) = \\mathrm{pmap}\\ (\\lambda i\\ hi\\;=>\\; f(\\langle i, hi\\rangle))\\ (\\mathrm{range}\\ n)\\ mem\\_range.1. $$$$
Lean4
theorem ofFn_eq_pmap {n} {f : Fin n → α} : ofFn f = pmap (fun i hi => f ⟨i, hi⟩) (range n) fun _ => mem_range.1 :=
by
rw [pmap_eq_map_attach]
exact ext_getElem (by simp) fun i hi1 hi2 => by simp [List.getElem_ofFn hi1]
