English
Let m, n be natural numbers and f : Fin m → α, g : Fin n → α. The encodings of f and g as lists are equal if and only if the dependent sums ⟨m, f⟩ and ⟨n, g⟩ are equal in Σ n, Fin n → α.
Русский
Пусть m, n — натуральные числа, f : Fin m → α, g : Fin n → α. Кодирование функций f и g в виде списков совпадает тогда и только тогда, когда пары ⟨m, f⟩ и ⟨n, g⟩ в сумме Σ n, Fin n → α равны.
LaTeX
$$$\\operatorname{ofFn}(f) = \\operatorname{ofFn}(g) \\iff \\langle m,f\\rangle = \\langle n,g\\rangle \\text{ in } \\Sigma n,\\; \\mathrm{Fin}(n) \\to \\alpha.$$$
Lean4
/-- `Fin.sigma_eq_iff_eq_comp_cast` may be useful to work with the RHS of this expression. -/
theorem ofFn_inj' {m n : ℕ} {f : Fin m → α} {g : Fin n → α} : ofFn f = ofFn g ↔ (⟨m, f⟩ : Σ n, Fin n → α) = ⟨n, g⟩ :=
Iff.symm <| equivSigmaTuple.symm.injective.eq_iff.symm
