uniqueDiffWithinAt_of_continuousLinearEquiv

English

Given an invertible derivative e', HasFDerivWithinAt f e' s x implies UniqueDiffWithinAt 𝕜 (Set.image f s) at f x.

Русский

При наличии инвертируемой производной e', HasFDerivWithinAt f e' s x влечет UniqueDiffWithinAt 𝕜 (Set.image f s) в f x.

LaTeX

$$$$ \\text{HasFDerivWithinAt } f e' s x \\Rightarrow \\text{UniqueDiffWithinAt } 𝕜 (\\text{Set.image } f s) $$$$

Lean4

theorem uniqueDiffWithinAt_of_continuousLinearEquiv (e' : E ≃L[𝕜] F) (h : HasFDerivWithinAt f (e' : E →L[𝕜] F) s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) : UniqueDiffWithinAt 𝕜 (f '' s) (f x) :=
  h.uniqueDiffWithinAt hs e'.surjective.denseRange

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