setToL1_simpleFunc_indicatorConst

English

For a measurable set s with finite measure, and x in E, the L1-image of the indicator function equals T s x.

Русский

Для измеримого множества s с конечной мерой и фиксированного x ∈ E, образ L1 индикатора равен T s x.

LaTeX

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

Lean4

theorem setToL1_simpleFunc_indicatorConst (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s)
    (hμs : μ s < ∞) (x : E) : setToL1 hT (simpleFunc.indicatorConst 1 hs hμs.ne x) = T s x :=
  by
  rw [setToL1_eq_setToL1SCLM]
  exact setToL1S_indicatorConst (fun s => hT.eq_zero_of_measure_zero) hT.1 hs hμs x

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