integral_eq_zero_iff_of_nonneg — Mathlib

English

The equivalence between lintegral equality and integral equality: for f: α → NNReal with Integrable f.toReal, ∫⁻ ENNReal.ofNNReal f ≤ ENNReal.ofNNReal b iff ∫ f ≤ b (toReal).

Русский

Эквивалентность равенств линтеграла и интеграла для вещественных значений NNReal: f: α → NNReal; Integrable; ∫⁻ ENNReal.ofNNReal f ≤ ENNReal.ofNNReal b ↔ ∫ f.toReal ≤ b.toReal.

LaTeX

$$$\\\\int⁻ a \\, ENNReal.ofNNReal (f(a)) \\, d\\\\mu \\\\le ENNReal.ofNNReal(b) \\\\Longleftrightarrow \\\\int a \\, (f(a)).toReal \\, d\\\\mu \\\\le b.toReal$$$

Lean4

theorem integral_eq_zero_iff_of_nonneg {f : α → ℝ} (hf : 0 ≤ f) (hfi : Integrable f μ) : ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
  integral_eq_zero_iff_of_nonneg_ae (Eventually.of_forall hf) hfi

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