hasDerivWithinAt_sub_const_iff — Mathlib

English

For any c, HasDerivWithinAt (f x − c) f' s x is equivalent to HasDerivWithinAt f f' s x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem hasDerivWithinAt_sub_const_iff (c : F) : HasDerivWithinAt (f · - c) f' s x ↔ HasDerivWithinAt f f' s x :=
  hasDerivAtFilter_sub_const_iff c

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