ofStar

Mathlib.Topology.Algebra.InfiniteSum.Constructions

URI: https://scilib.ai/kg/mathlib#Summable.ofStar

English

If the star-valued series of f is summable, then f itself is summable with respect to L.

Русский

Если сумма звёзд f по L суммируема, то и f суммируема по L.

LaTeX

$$$ Summable (\lambda b, \star (f b)) L \rightarrow Summable f L $$$

Lean4

theorem ofStar (hf : Summable (fun b ↦ Star.star (f b)) L) : Summable f L := by simpa only [star_star] using hf.star

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru