English
For a LinearOrder α, and a, b ∈ α, and predicate P, almost everywhere on the uIoc(a,b) set is equivalent to almost everywhere on Ioc(a,b) and on Ioc(b,a).
Русский
Для линейного порядка α и точек a,b, предикат P удовлетворяется почти всюду на унионно-включаемом интервале uIoc(a,b) тогда и только тогда, когда он удовлетворяется почти всюду на Ioc(a,b) и на Ioc(b,a).
LaTeX
$$$$\\forall a,b:\\alpha,\\; P:\\alpha\\to \\mathrm{Prop},\\;\\mathrm{ae}\\;\\mu\\bigl(\\{x:\\alpha\\mid x\\in Ι(a,b)\\rightarrow P(x)\\}\\bigr) \\iff \\Big(\\mathrm{ae}\\;\\mu(\\{x:\\alpha\\mid x\\in Ioc(a,b)\\rightarrow P(x)\\}) \\land \\mathrm{ae}\\;\\mu(\\{x:\\alpha\\mid x\\in Ioc(b,a)\\rightarrow P(x)\\})\\Big).$$$$
Lean4
/-- See also `MeasureTheory.ae_restrict_uIoc_iff`. -/
theorem ae_uIoc_iff [LinearOrder α] {a b : α} {P : α → Prop} :
(∀ᵐ x ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ x ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ x ∂μ, x ∈ Ioc b a → P x := by
simp only [uIoc_eq_union, mem_union, or_imp, eventually_and]
