English
For a family S: α → Submodule R M, x ∈ Finsupp.submodule S iff for all i, x(i) ∈ S(i).
Русский
Для семейства S: α → Submodule R M, x ∈ Finsupp.submodule S тогда и только тогда, когда для каждого i верно x(i) ∈ S(i).
LaTeX
$$$x \in \text{Finsupp.submodule } S \iff \forall i, x(i) \in S(i)$$$
Lean4
/-- Given a family `Sᵢ` of `R`-submodules of `M` indexed by a type `α`, this is the `R`-submodule
of `α →₀ M` of functions `f` such that `f i ∈ Sᵢ` for all `i : α`. -/
def submodule (S : α → Submodule R M) : Submodule R (α →₀ M)
where
carrier := {x | ∀ i, x i ∈ S i}
add_mem' hx hy i := (S i).add_mem (hx i) (hy i)
zero_mem' i := (S i).zero_mem
smul_mem' r _ hx i := (S i).smul_mem r (hx i)
