English
The outer measure of the half-open interval (a,b] equals the difference f(b) - f(a) translated into ENNReal.
Русский
Внешняя мера полупрозрачного интервала (a,b] равна разности f(b) - f(a) в ENNReal.
LaTeX
$$f.outer(Ioc(a,b)) = \operatorname{ofReal}(f(b) - f(a))$$
Lean4
theorem measurableSet_Ioi {c : ℝ} : MeasurableSet[f.outer.caratheodory] (Ioi c) :=
by
refine OuterMeasure.ofFunction_caratheodory fun t => ?_
refine le_iInf fun a => le_iInf fun b => le_iInf fun h => ?_
refine
le_trans (add_le_add (f.length_mono <| inter_subset_inter_left _ h) (f.length_mono <| diff_subset_diff_left h)) ?_
rcases le_total a c with hac | hac <;> rcases le_total b c with hbc | hbc
·
simp only [Ioc_inter_Ioi, f.length_Ioc, hac, hbc, le_refl, Ioc_eq_empty, max_eq_right, min_eq_left, Ioc_diff_Ioi,
f.length_empty, zero_add, not_lt]
·
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right, ← ENNReal.ofReal_add, f.mono hac,
f.mono hbc, sub_nonneg, sub_add_sub_cancel, le_refl, max_eq_right]
·
simp only [hbc, le_refl, Ioc_eq_empty, Ioc_inter_Ioi, min_eq_left, Ioc_diff_Ioi, f.length_empty, zero_add, or_true,
le_sup_iff, f.length_Ioc, not_lt]
·
simp only [hac, hbc, Ioc_inter_Ioi, Ioc_diff_Ioi, f.length_Ioc, min_eq_right, le_refl, Ioc_eq_empty, add_zero,
max_eq_left, f.length_empty, not_lt]
