English
An equivalent formulation of MDifferentiableAt in terms of continuity and differentiability in ext-chart coordinates.
Русский
Эквивалентная формулировка MDifferentiableAt через непрерывность и дифференцируемость в/extChart координатах.
LaTeX
$$$\text{mdifferentiableAt_iff'} (f) (x) : MDifferentiableAt I I' f x \iff \text{ContinuousAt } f x \wedge \text{DifferentiableWithinAt } 𝕜 (writtenInExtChartAt I I' x f) (\text{range } I) ((\text{extChartAt } I x) x)$$$
Lean4
theorem mdifferentiableAt_iff (f : M → M') (x : M) :
MDifferentiableAt I I' f x ↔
ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range I) ((extChartAt I x) x) :=
by
rw [MDifferentiableAt, liftPropAt_iff]
congrm _ ∧ ?_
simp [DifferentiableWithinAtProp, Set.univ_inter, Function.comp_assoc]
