English
For a fixed set s ⊆ α, the R-submodule of α →₀ M consisting of all finitely supported maps whose support is contained in s.
Русский
Для фиксированного множества s ⊆ α, состоящего из индексов, подмодуль над R в пространстве α →₀ M состоит из таких функций, опора которых лежит внутри s.
LaTeX
$$$\mathrm{supported}(M,R,s) = \{ p : α \to_0 M \mid p\text{ has finite support and } p\text{ supp} ⊆ s \}$$$
Lean4
/-- `Finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/
def supported (s : Set α) : Submodule R (α →₀ M)
where
carrier := {p | ↑p.support ⊆ s}
add_mem' {p q} hp
hq := by
classical
refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
rw [Finset.coe_union]
zero_mem' := by
simp only [subset_def, Finset.mem_coe, Set.mem_setOf_eq, mem_support_iff, zero_apply]
intro h ha
exact (ha rfl).elim
smul_mem' _ _ hp := Subset.trans (Finset.coe_subset.2 support_smul) hp
