measure_univ — Mathlib

English

For a Stieltjes f with limits l (bottom) and u (top), the measure of the whole real line is μ_f(ℝ) = ofReal(u - l).

Русский

Для f с пределами l (нижний) и u (верхний) мера всей ℝ равна ofReal(u - l).

LaTeX

$$μ_f(\mathbb{R}) = \operatorname{ofReal}(u - l)$$

Lean4

theorem measure_univ {l u : ℝ} (hfl : Tendsto f atBot (𝓝 l)) (hfu : Tendsto f atTop (𝓝 u)) :
    f.measure univ = ofReal (u - l) :=
  by
  refine tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_
  simp_rw [measure_Iic f hfl]
  exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)

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