English
Given l : (Σ i, αs i) →₀ M, the function splitSupport(l) is the finset of indices i that appear in the support of l; equivalently, the image of the first projection on the support.
Русский
Для l : (Σ i, αs i) →₀ M splitSupport(l) — это конечный набор индексов i, которые встречаются в опоре 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 `β`,
`split_support l` is the finset of indices in `ι` that appear in the support of `l`. -/
def splitSupport (l : (Σ i, αs i) →₀ M) : Finset ι :=
haveI := Classical.decEq ι
l.support.image Sigma.fst
