English
For every n, the map f ↦ ofFn f from functions Fin n → α to lists α is injective; equivalently, if ofFn f = ofFn g, then f = g.
Русский
Для каждого n отображение f ↦ ofFn f от функций Fin n → α в списки α инъективно; эквивалентно тому, что if ofFn f = ofFn g, то f = g.
LaTeX
$$$\\forall n\\in\\mathbb{N},\\ \\forall f,g:\\ \\mathrm{Fin}(n) \\to \\alpha,\\ \\operatorname{ofFn}(f) = \\operatorname{ofFn}(g) \\Rightarrow f = g.$$$
Lean4
/-- Note we can only state this when the two functions are indexed by defeq `n`. -/
theorem ofFn_injective {n : ℕ} : Function.Injective (ofFn : (Fin n → α) → List α) := fun f g h =>
eq_of_heq <| by rw [ofFn_inj'] at h; cases h; rfl
