hasFDerivAtFilter_const_add_iff — Mathlib

English

For fixed constant c, HasFDerivAtFilter (c + f) f' x L is equivalent to HasFDerivAtFilter f f' x L.

Русский

Для константы c равносильны HasFDerivAtFilter (c + f) f' x L и HasFDerivAtFilter f f' x L.

LaTeX

$$$$ HasFDerivAtFilter (c + f \cdot) f' x L \leftrightarrow HasFDerivAtFilter f f' x L.$$$$

Lean4

@[simp]
theorem hasFDerivAtFilter_const_add_iff (c : F) : HasFDerivAtFilter (c + f ·) f' x L ↔ HasFDerivAtFilter f f' x L := by
  simpa only [add_comm] using hasFDerivAtFilter_add_const_iff c

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