integrable_const_iff_isFiniteMeasure

English

If ‖c‖ ≠ 0 and ‖c‖ ≠ ∞, then the constant function is integrable iff μ is finite.

Русский

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

LaTeX

$$$\|c\| \neq 0 \land \|c\| \neq \infty \Rightarrow (\operatorname{Integrable}(\text{const } c, \mu) \iff \operatorname{IsFiniteMeasure}(\mu))$$$

Lean4

theorem integrable_const_iff_isFiniteMeasure {c : β} (hc : c ≠ 0) : Integrable (fun _ ↦ c) μ ↔ IsFiniteMeasure μ := by
  simp [integrable_const_iff, hc, isFiniteMeasure_iff]

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