English
If f is measurable, the ae-implication under μ.withDensity f is equivalent to an ae-implication under μ with the a.e. condition f ≠ 0.
Русский
Если f измерима, то эквивалентность Almost Everywhere утверждений между μ.withDensity f и μ сохраняется при условии f ≠ 0.
LaTeX
$$$(\\forall^\\infty x \\partial μ.withDensity f, p x) \\iff (\\forall^\\infty x \\partial μ, f x \\neq 0 \\to p x)$$$
Lean4
theorem ae_withDensity_iff {p : α → Prop} {f : α → ℝ≥0∞} (hf : Measurable f) :
(∀ᵐ x ∂μ.withDensity f, p x) ↔ ∀ᵐ x ∂μ, f x ≠ 0 → p x :=
ae_withDensity_iff' <| hf.aemeasurable