integral_sub — Mathlib

English

The integral of f − g equals the integral of f minus the integral of g, when f and g are integrable.

Русский

Интеграл от f − g равен интегралу f минус интеграл g при интегрируемости.

LaTeX

$$$$ \\int (f - g) \\, dμ = \\int f \\, dμ - \\int g \\, dμ $$$$

Lean4

theorem integral_sub {f g : α →ₛ E} (hf : Integrable f μ) (hg : Integrable g μ) :
    integral μ (f - g) = integral μ f - integral μ g :=
  setToSimpleFunc_sub _ weightedSMul_union hf hg

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