op

Mathlib.Topology.Algebra.InfiniteSum.Constructions

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

English

The property of summability is preserved by applying op: Summable f L iff Summable (op ∘ f) L.

Русский

Суммируемость сохраняется под действием оп: Summable f L эквивалентно Summable (op ∘ f) L.

LaTeX

$$$\\operatorname{Summable} f L \\iff \\operatorname{Summable}(\\lambda x, \\operatorname{op}(f x)) L$$$

Lean4

theorem op (hf : Summable f L) : Summable (op ∘ f) L :=
  hf.hasSum.op.summable

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

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

Разделы

Аффилиация

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