setToSimpleFunc_sub — Mathlib

English

Subtraction is compatible: setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g.

Русский

Вычитание сохраняется: setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g.

LaTeX

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

Lean4

theorem setToSimpleFunc_sub (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f g : α →ₛ E} (hf : Integrable f μ)
    (hg : Integrable g μ) : setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g :=
  by
  rw [sub_eq_add_neg, setToSimpleFunc_add T h_add hf, setToSimpleFunc_neg T h_add hg, sub_eq_add_neg]
  rw [integrable_iff] at hg ⊢
  intro x hx_ne
  rw [SimpleFunc.coe_neg, Pi.neg_def, ← Function.comp_def, preimage_comp, neg_preimage, Set.neg_singleton]
  refine hg (-x) ?_
  simp [hx_ne]

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