pderivCLM_eq_lineDeriv — Mathlib

English

The directional derivative pderivCLM 𝕜 m f equals the line derivative in direction m: pderivCLM 𝕜 m f x = lineDeriv ℝ f x m.

Русский

Директориальная производная pderivCLM 𝕜 m f равна линейной производной вдоль направления m: pderivCLM 𝕜 m f x = lineDeriv ℝ f x m.

LaTeX

$$$pderivCLM 𝕜\, m\, f\ x = lineDeriv ℝ f x m$$$

Lean4

theorem pderivCLM_eq_lineDeriv (m : E) (f : 𝓢(E, F)) (x : E) : pderivCLM 𝕜 m f x = lineDeriv ℝ f x m := by
  simp only [pderivCLM_apply, f.differentiableAt.lineDeriv_eq_fderiv]

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