English
If the supports of s_i are locally finite, then the supports of s_i · f_i are locally finite.
Русский
Если опоры функций s_i локально конечны, то опоры произведения s_i · f_i тоже локально конечны.
LaTeX
$$$\operatorname{LocallyFinite}(i \mapsto \operatorname{support}(s_i)) \Rightarrow \operatorname{LocallyFinite}\bigl(i \mapsto \operatorname{support}(s_i \cdot f_i)\bigr).$$$
Lean4
/-- If `a` and `b` are topologically nilpotent and commute,
then `a + b` is topologically nilpotent. -/
theorem add_of_commute [IsLinearTopology R R] {a b : R} (ha : IsTopologicallyNilpotent a)
(hb : IsTopologicallyNilpotent b) (h : Commute a b) : IsTopologicallyNilpotent (a + b) :=
by
simp only [IsTopologicallyNilpotent, atTop_basis.tendsto_iff IsLinearTopology.hasBasis_ideal, true_and]
intro I I_mem_nhds
obtain ⟨na, ha⟩ := ha.exists_pow_mem_of_mem_nhds I_mem_nhds
obtain ⟨nb, hb⟩ := hb.exists_pow_mem_of_mem_nhds I_mem_nhds
exact ⟨na + nb, fun m hm ↦ I.add_pow_mem_of_pow_mem_of_le_of_commute ha hb (le_trans hm (Nat.le_add_right _ _)) h⟩
