integrable_mul_const_iff — Mathlib

English

For any c with IsUnit, the function f ↦ f · c preserves integrability equivalence.

Русский

Для любого c, являются эквивалентными интегрируемость f и f · c, если c единица.

LaTeX

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

Lean4

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

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