English
A variant of dfinsuppProd_mem with additive-monoid homomorphisms as the g_i's.
Русский
Вариант dfinsuppProd_mem, где g_i являются гомоморфизмами сложения.
LaTeX
$$множество имеется, при условии выше$$
Lean4
/-- The supremum of a family of commutative additive submonoids is equal to the range of
`DFinsupp.sumAddHom`; that is, every element in the `iSup` can be produced from taking a finite
number of non-zero elements of `S i`, coercing them to `γ`, and summing them. -/
theorem iSup_eq_mrange_dfinsuppSumAddHom [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype) :=
by
apply le_antisymm
· apply iSup_le _
intro i y hy
exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩
· rintro x ⟨v, rfl⟩
exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop
