const_mul' — Mathlib

English

If f is integrable, then c • f is integrable in ENorm setting, under appropriate structure.

Русский

Если f интегрируема, то c · f интегрируема в контексте ENorm при наличии нужной структуры.

LaTeX

$$$\mathrm{Integrable}(f,\mu) \Rightarrow \mathrm{Integrable}(a \mapsto c \cdot f(a), \mu).$$$

Lean4

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

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