integral_comp_mul_sub — Mathlib

English

Using substitution with a negative, one obtains: ∫_a^b f(-c x) dx = c⁻¹ ∫_{-c b}^{-c a} f(u) du.

Русский

При использовании отрицательного множителя: ∫_a^b f(-c x) dx = c⁻¹ ∫_{-c b}^{-c а} f(u) du.

LaTeX

$$$$\int_{a}^{b} f(-c x) \, dx = c^{-1} \int_{-c b}^{-c a} f(u) \, du.$$$$

Lean4

@[simp]
theorem integral_comp_mul_sub (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (c * x - d)) = c⁻¹ • ∫ x in c * a - d..c * b - d, f x := by
  simpa only [sub_eq_add_neg] using integral_comp_mul_add f hc (-d)

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