integrable_const_iff_isFiniteMeasure_enorm

English

If a nonzero constant c is integrated over a finite measure μ, then the constant function is integrable if and only if μ is finite.

Русский

Если константа c не равна нулю и μ конечно, то константная функция интегрируема тогда и только тогда, когда μ конечна.

LaTeX

$$$\operatorname{Integrable}(\text{const } c, \mu) \iff \operatorname{IsFiniteMeasure}(\mu)$ (for nonzero c).$$

Lean4

theorem integrable_const_iff_isFiniteMeasure_enorm {c : ε} (hc : ‖c‖ₑ ≠ 0) (hc' : ‖c‖ₑ ≠ ∞) :
    Integrable (fun _ ↦ c) μ ↔ IsFiniteMeasure μ := by simp [integrable_const_iff_enorm hc', hc, isFiniteMeasure_iff]

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