setLIntegral_rnDeriv_le — Mathlib

English

For any set s, the integral of the RN-derivative over s with respect to ν is bounded by μ(s).

Русский

Для любого множества s интеграл RN-дериватив по ν на s не превосходит μ(s).

LaTeX

$$$\\int\\limits_{s} \\nu.\\mathrm{rnDeriv}(\\mu, x) \\, d\\nu(x) \\le μ(s)$$$

Lean4

theorem setLIntegral_rnDeriv_le (s : Set α) : ∫⁻ x in s, μ.rnDeriv ν x ∂ν ≤ μ s :=
  (withDensity_apply_le _ _).trans (Measure.le_iff'.1 (withDensity_rnDeriv_le μ ν) s)

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