English
Restriction of a function to a finite set s yields a finitely supported function with support contained in s and equal to the original function on s.
Русский
Ограничение функции к конечному множеству s даёт конечноподдерживаемую функцию, чья опора вложена в s и совпадает с оригиналом на s.
LaTeX
$$def onFinset (s) (f) (hf) : Finsupp α M$$
Lean4
/-- `Finsupp.onFinset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
The function must be `0` outside of `s`. Use this when the set needs to be filtered anyways,
otherwise a better set representation is often available. -/
def onFinset (s : Finset α) (f : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : α →₀ M
where
support := onFinset_support s f
toFun := f
mem_support_toFun := by classical simpa [onFinset_support_def]
