integral_pos_iff_support_of_nonneg

English

If f ≥ 0 a.e. and integrable, then ∫ f > 0 iff μ(support f) > 0.

Русский

Если f ≥ 0 a.e. и интегрируема, то ∫ f > 0 тогда и только тогда, когда μ(опорf) > 0.

LaTeX

$$$0 < \int a \\, f(a) \\, d\\\\mu \\\\iff 0 < \\\\mu(\\\\mathrm{Supp} f)$$$

Lean4

theorem integral_pos_iff_support_of_nonneg {f : α → ℝ} (hf : 0 ≤ f) (hfi : Integrable f μ) :
    (0 < ∫ x, f x ∂μ) ↔ 0 < μ (Function.support f) :=
  integral_pos_iff_support_of_nonneg_ae (Eventually.of_forall hf) hfi

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