ae_restrict_uIoc_eq — Mathlib

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]

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