hasMFDerivWithinAt_iff_hasFDerivWithinAt

English

HasMFDerivWithinAt is equivalent to HasFDerivWithinAt in Euclidean coordinates provided by the chart, i.e., the charted derivative matches the standard derivative within coordinate charts.

Русский

HasMFDerivWithinAt эквивалентно HasFDerivWithinAt в евклидовых координатах, заданных чартом; производная в чартах совпадает с обычной производной внутри координат.

LaTeX

$$$\mathrm{HasMFDerivWithinAt}(f,s,x,f') \iff \mathrm{HasFDerivWithinAt}(f,f',s,x).$$$

Lean4

theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt {f'} :
    HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x := by
  simpa only [HasMFDerivWithinAt, and_iff_right_iff_imp, mfld_simps] using HasFDerivWithinAt.continuousWithinAt

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