differentiableWithinAt_writtenInExtChartAt

English

DifferentiableWithinAtProp I (model of H) to I' (target chart) when the target is the model itself.

Русский

DifferentiableWithinAtProp для самоперекрестной модели и цели карты.

LaTeX

$$$\text{differentiableWithinAtProp_self_target } {f : H → E'} {s} {x} :\ \text{DifferentiableWithinAtProp } I \; I' \; f \; s \; x \Rightarrow \text{DifferentiableWithinAt } 𝕜 (f \circ I^{-1}) (I^{-1} s \cap \text{range } I) (I x)$$$

Lean4

theorem differentiableWithinAt_writtenInExtChartAt {f : M → M'} {x : M} (hf : MDifferentiableAt I I' f x) :
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range I) ((extChartAt I x) x) :=
  mdifferentiableAt_iff .. |>.1 hf |>.2

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