measure_Ioo — Mathlib

English

The measure of the half-open interval Ico(a,b) equals ofReal(leftLim f(b) - leftLim f(a)).

Русский

Мера Ico(a,b) равна ofReal(leftLim f(b) - leftLim f(a)).

LaTeX

$$μ_f(Ico(a,b)) = \operatorname{ofReal}(leftLim f(b) - leftLim f(a))$$

Lean4

@[simp]
theorem measure_Ioo {a b : ℝ} : f.measure (Ioo a b) = ofReal (leftLim f b - f a) :=
  by
  rcases le_or_gt b a with (hab | hab)
  · simp only [hab, measure_empty, Ioo_eq_empty, not_lt]
    symm
    simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]
  · have A : Disjoint (Ioo a b) { b } := by simp
    have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel
    have := f.measure_Ioc a b
    simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton, measure_union A (measurableSet_singleton b),
      Icc_self] at this
    rw [D, ENNReal.ofReal_add, add_comm] at this
    · simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]
    · simp only [f.mono.leftLim_le le_rfl, sub_nonneg]
    · simp only [f.mono.le_leftLim hab, sub_nonneg]

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