measure_Ioi — Mathlib

English

If f tends to a limit l at +∞, then μ_f(Ioi x) = ∞ for all x.

Русский

Если f стремится к пределу l при +∞, то μ_f(Ioi x) = ∞ для любого x.

LaTeX

$$μ_f(Ioi(x)) = ∞$$

Lean4

theorem measure_Ioi {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) : f.measure (Ioi x) = ofReal (l - f x) := by
  rw [← Ici_diff_left, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton, f.measure_Ici hf, ←
      ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)] <;>
    simp

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