ae_imp_of_ae_restrict — Mathlib

English

If p holds almost everywhere with respect to μ restricted to s, then p holds almost everywhere on μ under the condition x ∈ s → p(x).

Русский

Если p выполняется почти всюду относительно μ ограниченного до s, то p выполняется почти всюду относительно μ при условии x ∈ s → p(x).

LaTeX

$$$\forall x\, (x) : p(x) \text{ a.e. w.r.t. } μ|_s \implies \forall^\mathrm{a.e.}_{x} (x \in s \to p(x)) \text{ w.r.t. } μ.$$$

Lean4

theorem ae_imp_of_ae_restrict {s : Set α} {p : α → Prop} (h : ∀ᵐ x ∂μ.restrict s, p x) : ∀ᵐ x ∂μ, x ∈ s → p x :=
  by
  simp only [ae_iff] at h ⊢
  simpa [setOf_and, inter_comm] using measure_inter_eq_zero_of_restrict h

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