hasFDerivAt_natCast — Mathlib

English

Let n ∈ ℕ and x ∈ E. The derivative at x of the constant map n cast into F is the zero linear map.

Русский

Пусть n ∈ ℕ и x ∈ E. Производная в точке x константного отображения n, приводимого в F, равна нулевому линейному отображению.

LaTeX

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

Lean4

@[fun_prop]
theorem hasFDerivAt_natCast [NatCast F] (n : ℕ) (x : E) : HasFDerivAt (n : E → F) (0 : E →L[𝕜] F) x :=
  hasFDerivAt_const _ _

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