setToL1SCLM_const — Mathlib

English

For finite measure μ, the constant-indicator simple function is sent to T univ by setToL1SCLM.

Русский

При конечной мере μ простая функция-индикатор от всего пространства отправляется в T_univ через setToL1SCLM.

LaTeX

$$$\text{If } [IsFiniteMeasure\; μ] \text{ then } setToL1SCLM α E μ hT (simpleFunc.indicatorConst 1 MeasurableSet.univ (measure_ne_top μ _) x) = T univ x$$$

Lean4

theorem setToL1SCLM_const [IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (x : E) : setToL1SCLM α E μ hT (simpleFunc.indicatorConst 1 MeasurableSet.univ (measure_ne_top μ _) x) = T univ x :=
  setToL1S_const (fun _ => hT.eq_zero_of_measure_zero) hT.1 x

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