integrable_fun_smul_iff — Mathlib

English

If c ≠ 0, then for any f, Integrable (x ↦ c • f(x)) iff Integrable f.

Русский

Если c ≠ 0, тогда для любого f интегрируемость x ↦ c · f(x) эквивалентна интегрируемости f.

LaTeX

$$$c \neq 0 \Rightarrow \mathrm{Integrable}\left(x \mapsto c \cdot f(x)\right) \mu \Leftrightarrow \mathrm{Integrable}(f) \mu.$$$

Lean4

theorem integrable_fun_smul_iff [NormedDivisionRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : c ≠ 0)
    (f : α → β) : Integrable (fun x ↦ c • f x) μ ↔ Integrable f μ :=
  integrable_smul_iff hc f

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