pullbackWithin_eq_of_fderivWithin_eq

English

If V is differentiable within t and fderivWithin 𝕜 f s x is invertible, then pullbackWithin 𝕜 f V s is differentiable within s at x.

Русский

Если V дифференцируема внутри t и fderivWithin 𝕜 f s x обратима, то pullbackWithin 𝕜 f V s дифференцируема внутри s в точке x.

LaTeX

$$$ \\text{DifferentiableWithinAt } 𝕜\\; (pullbackWithin 𝕜 f V s)\\; s\\; x $$$

Lean4

theorem pullbackWithin_eq_of_fderivWithin_eq {f : E → F} {M : E ≃L[𝕜] F} {x : E} (hf : M = fderivWithin 𝕜 f s x)
    (V : F → F) : pullbackWithin 𝕜 f V s x = M.symm (V (f x)) := by simp [pullbackWithin, ← hf]

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