uniqueDiffWithinAt_extChartAt_target

English

At the point extChartAt I x x, there is UniqueDiffWithinAt 𝕜 on the target of extChartAt I x.

Русский

В точке (extChartAt I x x) внутри целевой области extChartAt I x существует уникальная дифференцируемость 𝕜.

LaTeX

$$$ UniqueDiffWithinAt\\ 𝕜\\ ((\\mathrm{extChartAt}\\ I\\ x).\\mathrm{target})\\ ((\\mathrm{extChartAt}\\ I\\ x).\\mathrm{toFun}\\ x)$$$

Lean4

theorem uniqueDiffWithinAt_extChartAt_target (x : M) :
    UniqueDiffWithinAt 𝕜 (extChartAt I x).target (extChartAt I x x) :=
  uniqueDiffOn_extChartAt_target x _ <| mem_extChartAt_target x

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