integral_neg — Mathlib

English

If HasIntegral I l f vol y holds, then integral I l f vol equals y.

Русский

Если HasIntegral выполняется для y, то интеграл равен y.

LaTeX

$$$\mathrm{integral\_eq}\; (h:\mathrm{HasIntegral}\; I\; l\; f\; vol\; y) : \mathrm{integral}(I,l,f,vol) = y$$$

Lean4

@[simp]
theorem integral_neg : integral I l (-f) vol = -integral I l f vol := by
  classical
    exact
    if h : Integrable I l f vol then h.hasIntegral.neg.integral_eq
    else by rw [integral, integral, dif_neg h, dif_neg (mt Integrable.of_neg h), neg_zero]

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