differentiableWithinAt_writtenInExtChartAt

English

The local invariance property of differentiability within at is preserved under smooth changes of charts.

Русский

Локальная инвариантность сохраняется при гладких переходах координат.

LaTeX

$$$\text{differentiableWithinAt_localInvariantProp} : (contDiffGroupoid 1 I).LocalInvariantProp (contDiffGroupoid 1 I') (DifferentiableWithinAtProp I I')$$$

Lean4

theorem differentiableWithinAt_writtenInExtChartAt {f : M → M'} {s : Set M} {x : M}
    (hf : MDifferentiableWithinAt I I' f s x) :
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).symm ⁻¹' s ∩ range I)
      ((extChartAt I x) x) :=
  mdifferentiableWithinAt_iff' .. |>.1 hf |>.2

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