ofFn_get — Mathlib

English

The vector built from a function f by ofFn is exactly f back in vector form.

Русский

Вектор, построенный из функции f через ofFn, совпадает с вектором, полученным из f.

LaTeX

$$$\mathrm{ofFn}\ (\mathrm{get}\ v) = v$$$

Lean4

@[simp]
theorem ofFn_get (v : Vector α n) : ofFn (get v) = v :=
  by
  rcases v with ⟨l, rfl⟩
  apply toList_injective
  dsimp
  simpa only [toList_ofFn] using List.ofFn_get _

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