English
Let p be a predicate on α. If the set {x | p(x)} is null-measurable with respect to μ restricted to s, then p holds μ-almost everywhere on s if and only if p holds μ-almost everywhere on α under the restriction to s in the implication form.
Русский
Пусть p : α → Правда. Если множество {x | p(x)} является нулевой измеримой относительно μ, ограниченного до s, то выполнение p на почти всюду по μ на s эквивалентно тому, что p выполняется почти всюду по μ на всём пространстве при учёте условия x ∈ s ⇒ p(x).
LaTeX
$$$\text{NullMeasurableSet}({x : α \mid p(x)}, μ|_s) \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 : NullMeasurableSet {x | p x} (μ.restrict s)) :
(∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=
by
simp only [ae_iff, ← compl_setOf, Measure.restrict_apply₀ hp.compl]
rw [iff_iff_eq]; congr with x; simp [and_comm]
