derivWithin_comp_const_add — Mathlib

English

Translation in the domain by a fixed a does not change the derivative within a shifted set.

Русский

Сдвиг аргумента на константу a не изменяет производную внутри области после соответствующего сдвига множества.

LaTeX

$$$\\mathrm{derivWithin}(f\\lvert\\!\\!\\; (a+\\cdot), s, x) = \\mathrm{derivWithin}(f, a+\\!\\!\\! s, a+x)$$$

Lean4

/-- Translation in the domain does not change the derivative. -/
theorem derivWithin_comp_const_add : derivWithin (f <| a + ·) s x = derivWithin f (a +ᵥ s) (a + x) := by
  simp only [derivWithin, fderivWithin_comp_add_left]

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