integrable_const_mul_iff — Mathlib

English

If f : α → 𝕜 is integrable, then f multiplied by a constant on the left is integrable.

Русский

Если f: α → 𝕜 интегрируема, то константа слева множит f остаётся интегрируемой.

LaTeX

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

Lean4

theorem integrable_const_mul_iff {c : 𝕜} (hc : IsUnit c) (f : α → 𝕜) :
    Integrable (fun x => c * f x) μ ↔ Integrable f μ :=
  hc.integrable_smul_iff f

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