ae_lt_top' — Mathlib

English

If f is AEMeasurable and its lintegral is finite, then f is finite almost everywhere.

Русский

Если f измеримо почти всюду и его линИнтеграл конечен, тогда f конечна почти повсюду.

LaTeX

$$$AEMeasurable\\ f\\ μ \\wedge ∫⁻ x, f(x) ∂μ \\neq ∞ \\Rightarrow ∀ᵐ x ∂μ, f(x) < ∞$$$

Lean4

theorem ae_lt_top' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (h2f : ∫⁻ x, f x ∂μ ≠ ∞) : ∀ᵐ x ∂μ, f x < ∞ :=
  by
  simp_rw [ae_iff, ENNReal.not_lt_top]
  exact measure_eq_top_of_lintegral_ne_top hf h2f

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