integral_neg — Mathlib

English

For any integrable function f: α → G, the integral of −f equals − the integral of f.

Русский

Для любой интегрируемой функции f: α → G интеграл от −f равен − интеграла от f.

LaTeX

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

Lean4

@[integral_simps]
theorem integral_neg (f : α → G) : ∫ a, -f a ∂μ = -∫ a, f a ∂μ :=
  by
  by_cases hG : CompleteSpace G
  · simp only [integral, hG, L1.integral]
    exact setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f
  · simp [integral, hG]

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