hasStrictFDerivAt_const_add_iff — Mathlib

English

A constant addition in the argument does not affect the strict derivative at x.

Русский

Добавление константы к аргументу не меняет строгий производный в x.

LaTeX

$$$$ HasStrictFDerivAt (\lambda x, c + f x) f' x \leftrightarrow HasStrictFDerivAt f f' x $$$$

Lean4

@[simp]
theorem hasStrictFDerivAt_const_add_iff (c : F) : HasStrictFDerivAt (c + f ·) f' x ↔ HasStrictFDerivAt f f' x := by
  simpa only [add_comm] using hasStrictFDerivAt_add_const_iff c

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