integral_comp_add_left — Mathlib

English

The smoothed integral with addition on the left reproduces the right shifted interval: ∫_a^b f(x + d) dx = ∫_{a + d}^{b + d} f(x) dx.

Русский

Смещение слева внутри интеграла эквивалентно смещению границ интегрирования: ∫_a^b f(x + d) dx = ∫_{a + d}^{b + d} f(x) dx.

LaTeX

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

Lean4

@[simp]
nonrec theorem integral_comp_add_left (d) : (∫ x in a..b, f (d + x)) = ∫ x in d + a..d + b, f x := by
  simpa only [add_comm d] using integral_comp_add_right f d

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