integral_sub' — Mathlib

English

Again, for integrable f and g, the integral of f − g equals the difference of the integrals.

Русский

Снова для интегрируемых функций 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 - g) a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ :=
  integral_sub hf hg

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