ae_restrict_iff'₀ — Mathlib

English

If s is null-measurable with respect to μ, then (∀ᵐ x ∂μ.restrict s, p x) iff (∀ᵐ x ∂μ, x ∈ s → p x).

Русский

Если s нулево-измеримо относительно μ, тогда (∀ почти все x в μ|_s, p x) эквивалентно (∀ почти все x в μ, x ∈ s → p x).

LaTeX

$$$\text{NullMeasurableSet}(s, μ) \Rightarrow (\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } μ|_s) \iff (\forall^\mathrm{a.e.}_{x} [x \in s \to p(x)] \text{ w.r.t. } μ).$$$

Lean4

theorem ae_restrict_iff'₀ {p : α → Prop} (hs : NullMeasurableSet s μ) :
    (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=
  by
  simp only [ae_iff, ← compl_setOf, restrict_apply₀' hs]
  rw [iff_iff_eq]; congr with x; simp [and_comm]

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