inv_smul_integral_comp_div — Mathlib

English

For any f and c, the smoothed integral identity holds: c⁻¹ • ∫_a^b f(x / c) dx = ∫_{a/c}^{b/c} f(x) dx, which is another form of the previous substitution.

Русский

Для любого f и скаляра c имеет место равенство: c⁻¹ • ∫_a^b f(x / c) dx = ∫_{a/c}^{b/c} f(x) dx.

LaTeX

$$$$c^{-1} \cdot \int_{a}^{b} f\left(\frac{x}{c}\right) dx = \int_{a/c}^{b/c} f(x) dx.$$$$

Lean4

@[simp]
theorem inv_smul_integral_comp_div (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_div]

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