integral_congr — Mathlib

English

If f and g coincide on [a,b], then their interval integrals on [a,b] are equal.

Русский

Если функции f и g совпадают на [a,b], то их интегралы по интервалу [a,b] равны.

LaTeX

$$$ f = g \\text{ on } [a,b] \\quad \\Rightarrow \\quad \\int_{a}^{b} f(x) \\, dμ = \\int_{a}^{b} g(x) \\, dμ $$$

Lean4

/-- If two functions are equal in the relevant interval, their interval integrals are also equal. -/
theorem integral_congr {a b : ℝ} (h : EqOn f g [[a, b]]) : ∫ x in a..b, f x ∂μ = ∫ x in a..b, g x ∂μ := by
  rcases le_total a b with hab | hab <;>
    simpa [hab, integral_of_le, integral_of_ge] using
      setIntegral_congr_fun measurableSet_Ioc (h.mono Ioc_subset_Icc_self)

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