hasFDerivAt_one — Mathlib

English

Let x ∈ E. The derivative at x of the constant map f(y) = 1 is the zero linear map.

Русский

Пусть x ∈ E. Производная по Фреше константного отображения f(y) = 1 в точке x равна нулевому линейному отображению.

LaTeX

$$$HasFDerivAt (1 : E \to F) (0 : E \toL[𝕜] F) x$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_one [One F] (x : E) : HasFDerivAt (1 : E → F) (0 : E →L[𝕜] F) x :=
  hasFDerivAt_const _ _

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