setToL1S_sub — Mathlib

English

Set difference is respected: setToL1S T (f - g) = setToL1S T f - setToL1S T g.

Русский

Разность сохраняется: setToL1S T (f - g) = setToL1S T f - setToL1S T g.

LaTeX

$$$$setToL1S T (f - g) = setToL1S T f - setToL1S T g.$$$$

Lean4

theorem setToL1S_sub {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
  rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]

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