hasStrictFDerivAt_sub_const_iff — Mathlib

English

Let f: E → F have a strict Fréchet derivative f' at x. Then for any c ∈ F, the map x ↦ f(x) − c has the same strict Fréchet derivative at x, namely f'. In particular, HasStrictFDerivAt (x ↦ f(x) − c) f' x is equivalent to HasStrictFDerivAt f f' x.

Русский

Пусть f: E → F имеет строгий Фреше-дифференциал в точке x с производной f'. Тогда для любого c ∈ F отображение x ↦ f(x) − c имеет ту же строгую Фреше-дифференцию в x, равную f'.

LaTeX

$$$ HasStrictFDerivAt (x \\mapsto f(x) - c) f' x \\iff HasStrictFDerivAt f f' x $$$

Lean4

@[simp]
theorem hasStrictFDerivAt_sub_const_iff (c : F) : HasStrictFDerivAt (f · - c) f' x ↔ HasStrictFDerivAt f f' x := by
  simp only [sub_eq_add_neg, hasStrictFDerivAt_add_const_iff]

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