measure_Ico — Mathlib

English

If f tends to l at −∞, then the measure of Iic(x) equals ofReal(f(x) - l): μ_f(Iic(x)) = ofReal(f(x) - l).

Русский

Если f стремится к l при −∞, то мера Iic(x) равна ofReal(f(x) - l).

LaTeX

$$μ_f(Iic(x)) = \operatorname{ofReal}(f(x) - l)$$

Lean4

@[simp]
theorem measure_Ico (a b : ℝ) : f.measure (Ico a b) = ofReal (leftLim f b - leftLim f a) :=
  by
  rcases le_or_gt b a with (hab | hab)
  · simp only [hab, measure_empty, Ico_eq_empty, not_lt]
    symm
    simp [ENNReal.ofReal_eq_zero, f.mono.leftLim hab]
  · have A : Disjoint { a } (Ioo a b) := by simp
    simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, f.mono.leftLim_le, measure_union A measurableSet_Ioo,
      f.mono.le_leftLim hab, ← ENNReal.ofReal_add]

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