English
For a linear order, the a.e. restriction on the union of uIoc equals the supremum of ae restrictions on Ioc intervals.
Русский
Для линейного порядка a.e. ограничение на объединение uIoc равно супремуму ae ограничений на интервалы Ioc.
LaTeX
$$$\\operatorname{ae}(\\mu\\restrict (\\uIoc a b)) = \\operatorname{ae}(\\mu\\restrict (Ioc a b)) \\sqcup \\operatorname{ae}(\\mu\\restrict (Ioc b a)).$$$
Lean4
theorem ae_restrict_uIoc_eq [LinearOrder α] (a b : α) :
ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a)) := by
simp only [uIoc_eq_union, ae_restrict_union_eq]