smul_integral_comp_mul_right — Mathlib

English

For any c, the integral of f(x + c) over [a, b] equals the integral of f over [a + c, b + c]. More precisely, ∫_a^b f(x + d) dx = ∫_{a+d}^{b+d} f(x) dx.

Русский

Для любого с интеграл функции f(x + d) по [a, b] равен интегралу f(x) по [a + d, b + d].

LaTeX

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

Lean4

@[simp]
theorem smul_integral_comp_mul_right (c) : (c • ∫ x in a..b, f (x * c)) = ∫ x in a * c..b * c, f x := by
  by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_right]

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