mul_const'

Mathlib.MeasureTheory.Function.L1Space.Integrable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Integrable.mul_const'

English

If f is integrable and c ≠ 0, then c • f is integrable and vice versa.

Русский

Если f интегрируема и c ≠ 0, то c • f интегрируема и наоборот.

LaTeX

$$$\text{Integrable}(f,\mu) \Rightarrow \forall c, \mathrm{Integrable}(c \cdot f,\mu).$$$

Lean4

theorem mul_const' {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) : Integrable (f * fun _ : α => c) μ :=
  Integrable.mul_const h c

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

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

Разделы

Аффилиация

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