integrable_smul_iff — Mathlib

English

If c is a unit in 𝕜, then c • f is integrable iff f is integrable.

Русский

Если c является единицей-обратимой в 𝕜, то c · f интегрируема тогда и только тогда, когда f интегрируема.

LaTeX

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

Lean4

theorem _root_.IsUnit.integrable_smul_iff [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜}
    (hc : IsUnit c) (f : α → β) : Integrable (c • f) μ ↔ Integrable f μ :=
  and_congr hc.aestronglyMeasurable_const_smul_iff (hasFiniteIntegral_smul_iff hc f)

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