measure_support_lt_top_of_lintegral_ne_top

English

If the lintegral of f is not top, then the support of f is finite in measure sense.

Русский

Если линеграль не бесконечна, то опора функции в мерном смысле конечна.

LaTeX

$$$f.\lintegral\,\mu \neq \infty \Rightarrow \mu(\operatorname{supp}(f)) < \infty$$$

Lean4

theorem measure_support_lt_top_of_lintegral_ne_top {f : α →ₛ ℝ≥0∞} (hf : f.lintegral μ ≠ ∞) : μ (support f) < ∞ :=
  by
  refine measure_support_lt_top f ?_
  rw [← finMeasSupp_iff]
  exact FinMeasSupp.of_lintegral_ne_top hf

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