restrict — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Filter.EventuallyEq.restrict {f g : α → δ} {s : Set α} (hfg : f =ᵐ[μ] g) : f =ᵐ[μ.restrict s] g := by
  -- note that we cannot use `ae_restrict_iff` since we do not require measurability

  refine hfg.filter_mono ?_
  rw [Measure.ae_le_iff_absolutelyContinuous]
  exact absolutelyContinuous_restrict

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