toSimpleFunc_indicatorConst — Mathlib

English

Theae equality states that the a.e. equality of toSimpleFunc(indicatorConst ...) with a piecewise constant function holds.

Русский

Утверждается, что почти везде выполняется равенство toSimpleFunc(indicatorConst ...) и кусочно-постоянной функции.

LaTeX

$$$ toSimpleFunc (indicatorConst p hs hμs c) =_{\\mu} (SimpleFunc.const _ c).piecewise s hs (SimpleFunc.const _ 0) $$$

Lean4

theorem toSimpleFunc_indicatorConst {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : E) :
    toSimpleFunc (indicatorConst p hs hμs c) =ᵐ[μ] (SimpleFunc.const _ c).piecewise s hs (SimpleFunc.const _ 0) :=
  Lp.simpleFunc.toSimpleFunc_toLp _ _

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