ae_restrict_mem₀ — Mathlib

English

If s is measurable, then almost surely x ∈ s under μ.restrict s.

Русский

Если s измеримо, то почти наверняка x принадлежит s при μ ограниченной до s.

LaTeX

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

Lean4

theorem ae_restrict_mem₀ (hs : NullMeasurableSet s μ) : ∀ᵐ x ∂μ.restrict s, x ∈ s :=
  (ae_restrict_iff'₀ hs).2 (Filter.Eventually.of_forall fun _ => id)

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