English
The measure of the open interval Ioo(a,b) equals f(b) - leftLim f(b) - f(a) plus the adjustment; equivalently μ_f(Ioo(a,b)) = ofReal(leftLim f(b) - f(a)).
Русский
Мера открытого интервала Ioo(a,b) равна ofReal(leftLim f(b) - f(a)).
LaTeX
$$μ_f(Ioo(a,b)) = \operatorname{ofReal}(\,leftLim f(b) - f(a)\,)$$
Lean4
@[simp]
theorem measure_Icc (a b : ℝ) : f.measure (Icc a b) = ofReal (f b - leftLim f a) :=
by
rcases le_or_gt a b with (hab | hab)
· have A : Disjoint { a } (Ioc a b) := by simp
simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ENNReal.ofReal_add, f.mono.leftLim_le,
measure_union A measurableSet_Ioc, f.mono hab]
· simp only [hab, measure_empty, Icc_eq_empty, not_le]
symm
simp [ENNReal.ofReal_eq_zero, f.mono.le_leftLim hab]
