integral_neg — Mathlib

English

The integral of the negated function over an interval equals the negation of the integral of the function over the interval.

Русский

Интеграл от функции с отрицанием равен минусу интеграла самой функции.

LaTeX

$$$\int_{a}^{b} (-f(x)) \, dμ = -\int_{a}^{b} f(x) \, dμ$$$

Lean4

@[simp]
nonrec theorem integral_neg : ∫ x in a..b, -f x ∂μ = -∫ x in a..b, f x ∂μ := by
  simp only [intervalIntegral, integral_neg]; abel

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