hasMFDerivAt_const — Mathlib

English

The derivative of a constant function is zero.

Русский

Дифференциал константной функции равен нулю.

LaTeX

$$$ HasMFDerivAt I I' (\lambda _:\ M => c) x 0 $$$

Lean4

theorem hasMFDerivAt_const (c : M') (x : M) :
    HasMFDerivAt I I' (fun _ : M => c) x (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
  by
  refine ⟨continuous_const.continuousAt, ?_⟩
  simp only [writtenInExtChartAt, Function.comp_def, hasFDerivWithinAt_const]

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