summable_op

Mathlib.Topology.Algebra.InfiniteSum.Constructions

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

English

The summability of a function and of its op-image are equivalent.

Русский

Суммируемость функции и её образа через op эквивалентны.

LaTeX

$$$\\operatorname{Summable}(f L) \\iff \\operatorname{Summable}(\\operatorname{op} \\circ f) L$$$

Lean4

@[simp]
theorem summable_op : (Summable (fun a ↦ op (f a)) L) ↔ Summable f L :=
  ⟨Summable.unop, Summable.op⟩

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

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

Разделы

Аффилиация

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