integral_interval_sub_left — Mathlib

English

For any d, ∫_a^b f(d − x) dx = ∫_{d−b}^{d−a} f(x) dx.

Русский

Для любого d выполняется тождество замены переменной с заменой x на d − x: ∫_a^b f(d − x) dx = ∫_{d−b}^{d−a} f(x) dx.

LaTeX

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

Lean4

theorem integral_interval_sub_left (hab : IntervalIntegrable f μ a b) (hac : IntervalIntegrable f μ a c) :
    ((∫ x in a..b, f x ∂μ) - ∫ x in a..c, f x ∂μ) = ∫ x in c..b, f x ∂μ :=
  sub_eq_of_eq_add' <| Eq.symm <| integral_add_adjacent_intervals hac (hac.symm.trans hab)

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