of_lintegral_ne_top — Mathlib

English

For simple f into ENNReal, under almost everywhere finiteness, FinMeasSupp μ is equivalent to f.lintegral μ < ∞.

Русский

Для простой функции, допускаемой в ENNReal, при почти всюду конечном значении, FinMeasSupp μ эквивалентно f.lintegral μ < ∞.

LaTeX

$$$\\mathrm{FinMeasSupp}(f,\\mu) \\iff f.\\lintegral\\,\\mu < \\infty$ (при условии $f$finite$ \\,a.e.$)$$

Lean4

theorem of_lintegral_ne_top {f : α →ₛ ℝ≥0∞} (h : f.lintegral μ ≠ ∞) : f.FinMeasSupp μ :=
  by
  refine finMeasSupp_iff.2 fun b hb => ?_
  rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h
  refine ENNReal.lt_top_of_mul_ne_top_right ?_ hb
  exact (lt_top_of_sum_ne_top h (Finset.mem_insert_self _ _)).ne

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