hasDerivAtFilter_add_const_iff — Mathlib

English

For any constant c, HasDerivAtFilter (f · + c) f' x L is equivalent to HasDerivAtFilter f f' x L.

Русский

Для любой константы c, HasDerivAtFilter (f · + c) f' x L эквивалентно HasDerivAtFilter f f' x L.

LaTeX

$$$HasDerivAtFilter (f \cdot + c) f' x L \iff HasDerivAtFilter f f' x L$$$

Lean4

@[simp]
theorem hasDerivAtFilter_add_const_iff (c : F) : HasDerivAtFilter (f · + c) f' x L ↔ HasDerivAtFilter f f' x L :=
  hasFDerivAtFilter_add_const_iff c

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