English
The support of the finitely supported function associated to a list l is exactly the set of indices i within the length of l for which the i-th element is nonzero.
Русский
Поддержка сопоставления типа finsupp к списку l состоит из тех индексов i, которые лежат в диапазоне длины списка и соответствуют ненулевым элементам списка.
LaTeX
$$$$ \\operatorname{support}(l\\toFinsupp) = \\{ i \\in \\mathrm{Finset.range}(\\mathrm{length}(l)) \\mid l_i \\neq 0 \\}. $$$$
Lean4
/-- Indexing into a `l : List M`, as a finitely-supported function,
where the support are all the indices within the length of the list
that index to a non-zero value. Indices beyond the end of the list are sent to 0.
This is a computable version of the `Finsupp.onFinset` construction.
-/
def toFinsupp : ℕ →₀ M where
toFun i := getD l i 0
support := {i ∈ Finset.range l.length | getD l i 0 ≠ 0}
mem_support_toFun
n := by
simp only [Ne, Finset.mem_filter, Finset.mem_range, and_iff_right_iff_imp]
contrapose!
exact getD_eq_default _ _
