English
For mappings between manifolds with corners, being C^n at a point x is equivalent to the map being continuous at x and its coordinate expression in charts being C^n on the target’s chart domain.
Русский
Для отображений между многообразиями с углами, быть $C^n$ в точке x эквивалентно тому, что отображение непрерывно в x и его координатное выражение в графах в области области цели является $C^n$.
LaTeX
$$$ContMDiffAt\, I\, I'\, n\, f\, x \;\iff\; (ContinuousAt\, f\, x) \wedge \\ ContDiffWithinAt\, 𝕜\, n\, (extChartAt I' (f x) \circ f \circ (extChartAt I x).symm)\, (range I)\, (extChartAt I x x)$$
Lean4
theorem contMDiffAt_iff {n : WithTop ℕ∞} {f : M → M'} {x : M} :
ContMDiffAt I I' n f x ↔
ContinuousAt f x ∧
ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x) :=
liftPropAt_iff.trans <| by rw [ContDiffWithinAtProp, preimage_univ, univ_inter]; rfl
