mfderivWithin_eq — Mathlib

English

The symmetric MDifferentiableWithinAt holds for continuous linear equivalences.

Русский

Для непрерывно линейных эквивалентностей справедливо симметричное MDifferentiableWithinAt.

LaTeX

$$MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (EquivLike.toFunLike.coe f) s x$$

Lean4

theorem mfderivWithin_eq (hs : UniqueMDiffWithinAt 𝓘(𝕜, E) s x) :
    mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = (f : E →L[𝕜] E') :=
  f.hasMFDerivWithinAt.mfderivWithin hs

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