summable_star_iff

Mathlib.Topology.Algebra.InfiniteSum.Constructions

URI: https://scilib.ai/kg/mathlib#summable_star_iff

English

The star of f is summable with respect to L if and only if f is summable with respect to L.

Русский

Суммируемость звезды f по L эквивалентна суммируемости f по L.

LaTeX

$$$ Summable (\star f) L \leftrightarrow Summable f L $$$

Lean4

@[simp]
theorem summable_star_iff : Summable (fun b ↦ star (f b)) L ↔ Summable f L :=
  ⟨Summable.ofStar, Summable.star⟩

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

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

Разделы

Аффилиация

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