toList_ofFn — Mathlib

English

The toList of a vector created by ofFn is the list of the function values.

Русский

toList от вектора, созданного функцией ofFn, равен списку значений функции.

LaTeX

$$$\\mathrm{toList}(\\mathrm{ofFn}(f)) = \\mathrm{List}.ofFn(f)$$$

Lean4

@[simp]
theorem toList_ofFn : ∀ {n} (f : Fin n → α), toList (ofFn f) = List.ofFn f
  | 0, f => by rw [ofFn, List.ofFn_zero, toList, nil]
  | n + 1, f => by rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

Похожие утверждения