setToSimpleFunc_neg — Mathlib

English

The operator is compatible with negation: setToSimpleFunc T (-f) = - setToSimpleFunc T f.

Русский

Оператор совместим с отрицанием: setToSimpleFunc T (-f) = - setToSimpleFunc T f.

LaTeX

$$$ setToSimpleFunc T (-f) = - setToSimpleFunc T f $$$

Lean4

theorem setToSimpleFunc_neg (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f : α →ₛ E} (hf : Integrable f μ) :
    setToSimpleFunc T (-f) = -setToSimpleFunc T f :=
  calc
    setToSimpleFunc T (-f) = setToSimpleFunc T (f.map Neg.neg) := rfl
    _ = -setToSimpleFunc T f :=
      by
      rw [map_setToSimpleFunc T h_add hf neg_zero, setToSimpleFunc, ← sum_neg_distrib]
      exact Finset.sum_congr rfl fun x _ => ContinuousLinearMap.map_neg _ _

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