withDensity_apply_eq_zero — Mathlib

English

Equivalent zero-density statement with measurable f: μ.withDensity f s = 0 iff μ({f ≠ 0} ∩ s) = 0.

Русский

Эквивалентное нулевой плотности утверждение для измеримой f: μ.withDensity f s = 0 тогда и только тогда, когда μ({f ≠ 0} ∩ s) = 0.

LaTeX

$$$\\mu.withDensity f s = 0 \\iff \\mu\\bigl(\\{x \\mid f(x) \\neq 0\\} \\cap s\\bigr) = 0$$$

Lean4

theorem withDensity_apply_eq_zero {f : α → ℝ≥0∞} {s : Set α} (hf : Measurable f) :
    μ.withDensity f s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0 :=
  withDensity_apply_eq_zero' <| hf.aemeasurable

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