ae_lt_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ae_lt_top {f : α → ℝ≥0∞} (hf : Measurable f) (h2f : ∫⁻ x, f x ∂μ ≠ ∞) : ∀ᵐ x ∂μ, f x < ∞ :=
  ae_lt_top' hf.aemeasurable h2f

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