ae_restrict_uIoc_iff — Mathlib

English

An equivalent statement to ae_restrict_uIoc_eq in terms of almost-everywhere on Ioc intervals.

Русский

Эквивалентность ae_restrict_uIoc_eq в терминах almost everywhere на интервалах Ioc.

LaTeX

$$$(\\forallᵐ x ∂μ.restrict (Ι a b), P x) \\iff (\\forallᵐ x ∂μ.restrict (Ioc a b), P x) ∧ (\\forallᵐ x ∂μ.restrict (Ioc b a), P x).$$$

Lean4

/-- See also `MeasureTheory.ae_uIoc_iff`. -/
theorem ae_restrict_uIoc_iff [LinearOrder α] {a b : α} {P : α → Prop} :
    (∀ᵐ x ∂μ.restrict (Ι a b), P x) ↔ (∀ᵐ x ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ x ∂μ.restrict (Ioc b a), P x := by
  rw [ae_restrict_uIoc_eq, eventually_sup]

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