integral_sub — Mathlib

English

For integrable f and g, the Bochner integral respects subtraction: ∫ (f − g) = ∫ f − ∫ g.

Русский

Для интегрируемых f и g справедлива разность под интегралом: ∫(f − g) = ∫ f − ∫ g.

LaTeX

$$$\int a, f(a) - g(a) \partial\mu = \int a, f(a) \partial\mu - \int a, g(a) \partial\mu$$$

Lean4

theorem integral_sub {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) :
    ∫ a, f a - g a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ :=
  by
  by_cases hG : CompleteSpace G
  · simp only [integral, hG, L1.integral]
    exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg
  · simp [integral, hG]

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