lintegral_pos_iff_support — Mathlib

English

For Measurable f, 0 < ∫ f dμ iff 0 < μ(support f).

Русский

Для измеримой f: 0 < ∫ f dμ тогда и только тогда, когда μ(support f) > 0.

LaTeX

$$$0 < \\int f \\, d\\mu \\;\\Leftrightarrow\\; 0 < \\mu(\\mathrm{supp}\,f)$$$

Lean4

theorem lintegral_pos_iff_support {f : α → ℝ≥0∞} (hf : Measurable f) :
    (0 < ∫⁻ a, f a ∂μ) ↔ 0 < μ (Function.support f) := by
  simp [pos_iff_ne_zero, hf, Filter.EventuallyEq, ae_iff, Function.support]

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