setToFun_neg — Mathlib

English

The setToFun operator respects negation: setToFun μ T hT (−f) = − setToFun μ T hT f.

Русский

Оператор setToFun сохраняет отрицание: setToFun(μ, T, hT)(−f) = − setToFun(μ, T, hT)(f).

LaTeX

$$$\mathrm{setToFun}(\mu, T)\,h_T\,(-f) = -\mathrm{setToFun}(\mu, T)\,h_T\,f$$$

Lean4

theorem setToFun_neg (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : setToFun μ T hT (-f) = -setToFun μ T hT f :=
  by
  by_cases hf : Integrable f μ
  · rw [setToFun_eq hT hf, setToFun_eq hT hf.neg, Integrable.toL1_neg, (L1.setToL1 hT).map_neg]
  · rw [setToFun_undef hT hf, setToFun_undef hT, neg_zero]
    rwa [← integrable_neg_iff] at hf

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