smul_measure_nnreal

Mathlib.MeasureTheory.Function.L1Space.Integrable

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

English

If f is Integrable w.r.t μ, then for any NNReal c, f is Integrable w.r.t c•μ.

Русский

Если f интегрируема по μ, то для любого NNReal c функция f интегрируема по c • μ.

LaTeX

$$Integrable f μ → ∀ c ∈ NNReal, Integrable f (c • μ).$$

Lean4

@[fun_prop]
theorem smul_measure_nnreal {f : α → ε} (h : Integrable f μ) {c : ℝ≥0} : Integrable f (c • μ) :=
  by
  apply h.smul_measure
  simp

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

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

Разделы

Аффилиация

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