setLIntegral_pos_iff — Mathlib

English

For f measurable, 0 < ∫_s f dμ iff 0 < μ(support f ∩ s).

Русский

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

LaTeX

$$$0 < \\int_s f \\, d\\mu \\\\iff 0 < \\mu(\\mathrm{supp}\\,f \\cap s)$$$

Lean4

theorem setLIntegral_pos_iff {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} :
    0 < ∫⁻ a in s, f a ∂μ ↔ 0 < μ (Function.support f ∩ s) := by
  rw [lintegral_pos_iff_support hf, Measure.restrict_apply (measurableSet_support hf)]

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