setToL1S_add — Mathlib

English

If s is measurable and μ(s) < ∞, then setToL1S T (indicatorConst 1 s μ x) = T s x.

Русский

Если s измеримо и μ(s) < ∞, то setToL1S T(indicatorConst 1 s μ x) = T s x.

LaTeX

$$$$setToL1S T\big(\mathrm{indicatorConst}(1)_{s}\;\mu\neq\top\,x\big) = T(s) x.$$$$

Lean4

theorem setToL1S_add (T : Set α → E →L[ℝ] F) (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (f g : α →₁ₛ[μ] E) : setToL1S T (f + g) = setToL1S T f + setToL1S T g :=
  by
  simp_rw [setToL1S]
  rw [← SimpleFunc.setToSimpleFunc_add T h_add (SimpleFunc.integrable f) (SimpleFunc.integrable g)]
  exact SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) (add_toSimpleFunc f g)

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