hasStrictFDerivAt_const — Mathlib

English

The derivative of a constant map is identically zero.

Русский

Производная константной отображения равна нулю повсюду.

LaTeX

$$$ fderiv 𝕜 (\lambda x. c) x = 0 \quad \text{for any } c \in F.$$$

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_const (c : F) (x : E) : HasStrictFDerivAt (fun _ => c) (0 : E →L[𝕜] F) x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun _ => by simp only [zero_apply, sub_self, Pi.zero_apply]

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