integral_comp_sub_left — Mathlib

English

For any f: R → E integrable on [a,b], and any d ∈ R, we have ∫_a^b f(d − x) dx = ∫_{d−b}^{d−a} f(x) dx.

Русский

Для любой интегрируемой функции f: ℝ → E на [a,b] имеем ∫_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

@[simp]
theorem integral_comp_sub_left (d) : (∫ x in a..b, f (d - x)) = ∫ x in d - b..d - a, f x := by
  simpa only [one_mul, one_smul, inv_one] using integral_comp_sub_mul f one_ne_zero d

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