measure_Iio_of_tendsto_atBot_atBot

English

If f has finite limits l and u at the bottom and top, then μ_f(ℝ) = ofReal(u - l).

Русский

Если f имеет пределы l и u на дне и вершине, то μ_f(ℝ) = ofReal(u - l).

LaTeX

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

Lean4

theorem measure_Iio_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) : f.measure (Iio x) = ∞ :=
  by
  rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf (x - 1)]
  exact measure_mono <| Set.Iic_subset_Iio.mpr <| sub_one_lt x

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