setToL1S_neg — Mathlib

English

The operator is linear with respect to negation: setToL1S T (-f) = - setToL1S T f.

Русский

Линейный оператор по отношению к отрицанию: setToL1S T(-f) = - setToL1S T f.

LaTeX

$$$$setToL1S T(-f) = -\,setToL1S T f.$$$$

Lean4

theorem setToL1S_neg {T : Set α → E →L[ℝ] F} (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (f : α →₁ₛ[μ] E) : setToL1S T (-f) = -setToL1S T f :=
  by
  simp_rw [setToL1S]
  have : simpleFunc.toSimpleFunc (-f) =ᵐ[μ] ⇑(-simpleFunc.toSimpleFunc f) := neg_toSimpleFunc f
  rw [SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) this]
  exact SimpleFunc.setToSimpleFunc_neg T h_add (SimpleFunc.integrable f)

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