inv_smul_integral_comp_div_add — Mathlib

English

For any function f and nonzero c, the identity with inv scalar multiplication holds: c⁻¹ • ∫_a^b f(x/c) dx = ∫_{a/c}^{b/c} f(x) dx.

Русский

Для любого 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_add (c d) : (c⁻¹ • ∫ x in a..b, f (x / c + d)) = ∫ x in a / c + d..b / c + d, f x :=
  by by_cases hc : c = 0 <;> simp [hc, integral_comp_div_add]

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