piecewise_ae_eq_restrict — Mathlib

English

If s is measurable, then the piecewise function that equals f on s and g outside s is ae-equal to f with respect to the restricted measure μ|_s.

Русский

Если s измеримо, то функция piecewise f g равна почти наверняка f относительно ограниченной меры μ|_s.

LaTeX

$$$ \\text{piecewise } s\, f\, g =_{\\mathrm{ae}}^{\\mu|_s} f $$$

Lean4

theorem piecewise_ae_eq_restrict [DecidablePred (· ∈ s)] (hs : MeasurableSet s) : piecewise s f g =ᵐ[μ.restrict s] f :=
  by
  rw [ae_restrict_eq hs]
  exact (piecewise_eqOn s f g).eventuallyEq.filter_mono inf_le_right

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