piecewise_ae_eq_restrict_compl — Mathlib

English

If s is measurable, then the piecewise function is ae-equal to g with respect to μ|_{s^c}.

Русский

Если s измеримо, то piecewise f g равна a.e. для μ|_{s^c} функции g.

LaTeX

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

Lean4

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

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