hasDerivAtFilter_sub_const_iff — Mathlib

English

For any constant c, HasDerivAtFilter (fun x ↦ f x − c) f' x L holds if and only if HasDerivAtFilter f f' x L.

Русский

Для любого константного c верно, что HasDerivAtFilter (функция x ↦ f x − c) f' x L эквивалентно HasDerivAtFilter f f' x L.

LaTeX

$$$$ HasDerivAtFilter (\lambda x, f x - c) f' x L \iff HasDerivAtFilter f f' x L. $$$$

Lean4

@[simp]
theorem hasDerivAtFilter_sub_const_iff (c : F) :
    HasDerivAtFilter (fun x ↦ f x - c) f' x L ↔ HasDerivAtFilter f f' x L :=
  hasFDerivAtFilter_sub_const_iff c

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