unop

Mathlib.Topology.Algebra.InfiniteSum.Constructions

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

English

If f is summable, then unop ∘ f is summable.

Русский

Если f суммируема, то unop ∘ f суммируема.

LaTeX

$$$\\operatorname{Summable}(f) \\Rightarrow \\operatorname{Summable}(\\operatorname{unop} \\circ f)$$$

Lean4

theorem unop {f : β → αᵐᵒᵖ} (hf : Summable f L) : Summable (unop ∘ f) L :=
  hf.hasSum.unop.summable

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

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

Разделы

Аффилиация

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