ae_restrict_of_ae — Mathlib

English

If p holds almost everywhere under μ, then p holds almost everywhere under μ.restrict s.

Русский

Если p выполняется почти всюду по μ, то p выполняется почти всюду по μ|_s.

LaTeX

$$$\forall^\mathrm{a.e.}_{x} \ p(x) \text{ w.r.t. } μ \Rightarrow \forall^\mathrm{a.e.}_{x} \ p(x) \text{ w.r.t. } μ|_s.$$$

Lean4

theorem ae_restrict_of_ae {s : Set α} {p : α → Prop} (h : ∀ᵐ x ∂μ, p x) : ∀ᵐ x ∂μ.restrict s, p x :=
  h.filter_mono (ae_mono Measure.restrict_le_self)

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