ae_restrict_iff — Mathlib

English

Let p be a predicate with {x | p(x)} a measurable set. Then (∀ᵐ x ∂μ.restrict s, p x) holds if and only if (∀ᵐ x ∂μ, x ∈ s → p x).

Русский

Пусть p : α → Prop и {x | p(x)} измеримо. Тогда (∀ᵐ x ∂μ|_s, p x) эквивалентно (∀ᵐ x ∂μ, x ∈ s → p x).

LaTeX

$$$\text{MeasurableSet} \{x : α \mid p(x)\} \Rightarrow \Big( \forall^\mathrm{a.e.}_{x} \; p(x) \text{ (w.r.t. } μ|_s) \Big) \iff \Big( \forall^\mathrm{a.e.}_{x} \; [x \in s \to p(x)] \text{ (w.r.t. } μ) \Big).$$$

Lean4

theorem ae_restrict_iff {p : α → Prop} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=
  ae_restrict_iff₀ hp.nullMeasurableSet

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