English
For AddZeroClass M, the additive submonoid generated by all finitely supported singletons equals the top element; i.e., every finitely supported function is a finite sum of singleton functions.
Русский
Для AddZeroClass M аддитивная подмономиальная кость, порождённая всеми единичными функциями с конечной опорой, равна току; то есть любая функция с конечной опорой выражима как сумма конечного числа одиночек.
LaTeX
$$$\\operatorname{AddSubmonoid.closure} (\\{ f : \\alpha \\to_0 M \\mid \\exists a,b, f = \\mathrm{single}(a,b) \\}) = \\top$$$
Lean4
@[simp]
theorem add_closure_setOf_eq_single : AddSubmonoid.closure {f : α →₀ M | ∃ a b, f = single a b} = ⊤ :=
top_unique fun x _hx =>
Finsupp.induction x (AddSubmonoid.zero_mem _) fun a b _f _ha _hb hf =>
AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure <| ⟨a, b, rfl⟩) hf
