integral_of_ge — Mathlib

English

If f is not AEStronglyMeasurable on μ restricted to Ioc a b, then the interval integral over [a,b] is zero.

Русский

Если f не AEStronglyMeasurable на μ, ограниченном Ioc a b, то интервальный интеграл по [a,b] равен нулю.

LaTeX

$$$Not (AEStronglyMeasurable(f, μ|_{Ioc(a,b)})) \\Rightarrow \\int x \\in a..b f(x) \\partial\\mu = 0$$$

Lean4

theorem integral_of_ge (h : b ≤ a) : ∫ x in a..b, f x ∂μ = -∫ x in Ioc b a, f x ∂μ := by
  simp only [integral_symm b, integral_of_le h]

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