contMDiffWithinAt_iff_contDiffWithinAt

English

On a chart, continuity of higher-order differentiability (ContMDiffWithinAt) between two charted spaces is equivalent to the standard ContDiffWithinAt for the underlying Banach-space model.

Русский

На чарте изоморфизм непрерывной дифференциации порядка n между двумя моделями эквивалентен обычному ContDiffWithinAt для базовой банах-пространственной модели.

LaTeX

$$$\ContMDiffWithinAt I I' n f s x \;\iff\; \ContDiffWithinAt 𝕜 n f s x$$$

Lean4

theorem contMDiffWithinAt_iff_contDiffWithinAt {f : E → E'} {s : Set E} {x : E} :
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  by
  simp +contextual only [ContMDiffWithinAt, liftPropWithinAt_iff', ContDiffWithinAtProp, iff_def, mfld_simps]
  exact ContDiffWithinAt.continuousWithinAt

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