English
A standard consequence is that splitSupport(l) is exactly the set of indices that occur in the support of l, projected to the index set.
Русский
Следствие: splitSupport(l) совпадает с множеством индексов, которые встречаются в опоре l, проецированным на множество индексов.
LaTeX
$$$\\mathrm{splitSupport}(l) = \\mathrm{image}_{\\Sigma}(\\mathrm{fst})(\\mathrm{support}(l))$$$
Lean4
/-- Given `l`, a finitely supported function from the sigma type `Σ i, αs i` to `β` and
an `ι`-indexed family `g` of functions from `(αs i →₀ β)` to `γ`, `split_comp` defines a
finitely supported function from the index type `ι` to `γ` given by composing `g i` with
`split l i`. -/
def splitComp [Zero N] (g : ∀ i, (αs i →₀ M) → N) (hg : ∀ i x, x = 0 ↔ g i x = 0) : ι →₀ N
where
support := splitSupport l
toFun i := g i (split l i)
mem_support_toFun := by
intro i
rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]
