mfderiv — Mathlib

English

The mfderivWithin equals the fderivWithin evaluation with chart coordinates when h is differentiable within at.

Русский

mfderivWithin совпадает со значением fderivWithin в координатах диаграммы, когда есть дифференцируемость внутри множеств.

LaTeX

$$$ (hxs : UniqueMDiffWithinAt I s x) (h : MDifferentiableWithinAt I I' f s x) : mfderivWithin I I' f s x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f :) ((extChartAt I x).symm ⁻¹' s \cap range I) ((extChartAt I x) x) $$$

Lean4

protected theorem mfderiv (h : MDifferentiableAt I I' f x) :
    mfderiv I I' f x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f :) (range I) ((extChartAt I x) x) := by
  simp only [mfderiv, h, if_pos]

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