summable_star_iff'

Mathlib.Topology.Algebra.InfiniteSum.Constructions

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

English

The same equivalence as above, phrased as a simplification: Summable (star f) L is equivalent to Summable f L.

Русский

Та же эквивалентность: Summable(звезда f) по L эквивалентно Summable f по L.

LaTeX

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

Lean4

@[simp]
theorem summable_star_iff' : Summable (star f) L ↔ Summable f L :=
  summable_star_iff

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

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

Разделы

Аффилиация

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