hasMFDerivAt_iff_hasFDerivAt — Mathlib

English

At a point x, HasMFDerivAt is equivalent to HasFDerivAt in coordinates provided by extChartAt, i.e., differential exists with chain rule in chart coordinates.

Русский

В точке x HasMFDerivAt эквивалентно HasFDerivAt в координатах чарта; существует производная с правилом для композиции в координатах чарта.

LaTeX

$$$\mathrm{HasMFDerivAt}(f,x,f') \iff \mathrm{HasFDerivAt}(f,f',x).$$$

Lean4

theorem hasMFDerivAt_iff_hasFDerivAt {f'} : HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x := by
  rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]

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