derivWithin_const_sub — Mathlib

English

For any c, HasDerivWithinAt (λ x, f x − c) f' s x iff HasDerivWithinAt f f' s x.

Русский

Для любого c выполняется эквивалентность HasDerivWithinAt (λ x, f x − c) f' s x эквивалентно HasDerivWithinAt f f' s x.

LaTeX

$$$$ HasDerivWithinAt (\lambda x, f x - c) f' s x \iff HasDerivWithinAt f f' s x. $$$$

Lean4

theorem derivWithin_const_sub (c : F) : derivWithin (fun y ↦ c - f y) s x = -derivWithin f s x := by
  simp [sub_eq_add_neg, derivWithin.fun_neg]

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