rnDeriv_ne_top — Mathlib

English

Radon–Nikodym derivative μ.rnDer ν is ν-almost everywhere not equal to ∞.

Русский

Радон-Никодимов производный μ к ν не равен бесконечности почти всюду по ν.

LaTeX

$$$\\forall^† x, \\; μ.rnDer ν(x) \\neq ∞\\; \\text{for } ν\\text{-a.e. } x$$$

Lean4

theorem rnDeriv_ne_top (μ ν : Measure α) [SigmaFinite μ] : ∀ᵐ x ∂ν, μ.rnDeriv ν x ≠ ∞ := by
  filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx using hx.ne

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