abs

Mathlib.Topology.Algebra.InfiniteSum.Order

URI: https://scilib.ai/kg/mathlib#Multipliable.abs

English

If f is Multipliable, then its absolute value is Multipliable.

Русский

Если функция f суммируема, то её модуль |f| также суммируем по умножению.

LaTeX

$$$$\\text{Multipliable}(f) \\rightarrow \\text{Multipliable}(|f|).$$$$

Lean4

theorem abs (hf : Multipliable f) : Multipliable (|f ·|) :=
  let ⟨x, hx⟩ := hf;
  ⟨|x|, hx.abs⟩

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

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

Разделы

Аффилиация

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