setToFun_sub — Mathlib

English

If μ = 0, then setToFun μ T hT f = 0 for any f.

Русский

Если мера μ равна нулю, то setToFun μ T hT f = 0 для любого f.

LaTeX

$$$\text{If } \mu = 0,\ \mathrm{setToFun}(\mu, T)\,h_T\,f = 0$$$

Lean4

theorem setToFun_sub (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hg : Integrable g μ) :
    setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g := by
  rw [sub_eq_add_neg, sub_eq_add_neg, setToFun_add hT hf hg.neg, setToFun_neg hT g]

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