of_mem_Icc — Mathlib

English

If μ is finite and X maps into the closed interval [a,b] a.e., then X is integrable.

Русский

Если μ конечна и X принимает значения в замкнутом интервале [a,b] почти всюду, то X интегрируема.

LaTeX

$$$\operatorname{IsFiniteMeasure}(\mu) \Rightarrow (\forall a,b \in \mathbb{R}, X(\omega) \in [a,b] a.e. \Rightarrow \operatorname{Integrable}(X, \mu))$$$

Lean4

theorem of_mem_Icc [IsFiniteMeasure μ] (a b : ℝ) {X : α → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) :
    Integrable X μ :=
  ⟨hX.aestronglyMeasurable, .of_mem_Icc a b h⟩

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