const_mul — Mathlib

English

If f : α → 𝕜 is integrable, then for any c, the function x ↦ f(x) * c is integrable.

Русский

Если f: α → 𝕜 интегрируема, то ∀ c, функция x ↦ f(x) c интегрируема.

LaTeX

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

Lean4

@[fun_prop]
theorem const_mul {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) : Integrable (fun x => c * f x) μ :=
  h.smul c

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