hasMFDerivWithinAt_const — Mathlib

English

The derivative within a set of a constant map is zero.

Русский

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

LaTeX

$$$ mfderivWithin I I' (\lambda _ : M => c) s x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) $$$

Lean4

theorem hasMFDerivWithinAt_const (c : M') (s : Set M) (x : M) :
    HasMFDerivWithinAt I I' (fun _ : M => c) s x (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
  (hasMFDerivAt_const c x).hasMFDerivWithinAt

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