setToL1S_add_left' — Mathlib

English

If T'' s = T s + T' s for all s with μ s finite, then setToL1S T'' f = setToL1S T f + setToL1S T' f.

Русский

Если на каждом измеримом множестве с конечной мерой T'' s = T s + T' s, то setToL1S T'' f = setToL1S T f + setToL1S T' f.

LaTeX

$$$$\text{If } T''(s) = T(s) + T'(s) \text{ for all } s \text{ with } μ(s) < ∞,\; f: α →₁ₛ[μ] E, \quad setToL1S(T'')(f) = setToL1S(T)(f) + setToL1S(T')(f).$$$$

Lean4

theorem setToL1S_add_left' (T T' T'' : Set α → E →L[ℝ] F) (h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s)
    (f : α →₁ₛ[μ] E) : setToL1S T'' f = setToL1S T f + setToL1S T' f :=
  SimpleFunc.setToSimpleFunc_add_left' T T' T'' h_add (SimpleFunc.integrable f)

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