essSup_piecewise — Mathlib

English

If ν ≤ μ, then essSup f ν ≤ essSup f μ.

Русский

Если ν ≤ μ, тогда essSup f ν ≤ essSup f μ.

LaTeX

$$$$ \\operatorname{essSup} f \\nu \\le \\operatorname{essSup} f \\mu \\quad \\text{if } \\nu \\le \\mu $$$$

Lean4

theorem essSup_piecewise {s : Set α} [DecidablePred (· ∈ s)] {g} (hs : MeasurableSet s) :
    essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ)) := by
  simp only [essSup, limsup_piecewise, blimsup_eq_limsup, ae_restrict_eq, hs, hs.compl]; rfl

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