hasFDerivWithinAt_sub_const_iff — Mathlib

English

For any c ∈ F, HasFDerivWithinAt (x ↦ f(x) − c) f' s x is equivalent to HasFDerivWithinAt f f' s x; subtracting a constant does not affect the derivative within a set.

Русский

Для любого c ∈ F равносильно HasFDerivWithinAt (x ↦ f(x) − c) f' s x и HasFDerivWithinAt f f' s x; вычитание константы не изменяет производную внутри множества.

LaTeX

$$$ HasFDerivWithinAt (x \\mapsto f(x) - c) f' s x \\iff HasFDerivWithinAt f f' s x $$$

Lean4

@[simp]
theorem hasFDerivWithinAt_sub_const_iff (c : F) : HasFDerivWithinAt (f · - c) f' s x ↔ HasFDerivWithinAt f f' s x :=
  hasFDerivAtFilter_sub_const_iff c

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