setToL1_eq_setToL1SCLM — Mathlib

English

IndicatorConst-labeled simple functions yield exact T-values for finite-measure sets.

Русский

Индикаторные простые функции дают точные значения T на множестве с конечной мерой.

LaTeX

$$$$setToL1S T (simpleFunc.indicatorConst 1 hs hμs.ne x) = T s x.$$$$

Lean4

theorem setToL1_eq_setToL1SCLM (hT : DominatedFinMeasAdditive μ T C) (f : α →₁ₛ[μ] E) :
    setToL1 hT f = setToL1SCLM α E μ hT f :=
  uniformly_extend_of_ind simpleFunc.isUniformInducing (simpleFunc.denseRange one_ne_top)
    (setToL1SCLM α E μ hT).uniformContinuous _

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