English
A differentiability in the model sense is equivalent to continuity at x plus differentiability within ext-chart at x.
Русский
Дифференцируемость в модели эквивалентна непрерывности в точке x и дифференцируемости в экст-диаграмме.
LaTeX
$$$\text{MDifferentiableAt } I I' f x \iff \big( \text{ContinuousAt } f x \wedge \text{DifferentiableWithinAt } 𝕜 (writtenInExtChartAt I I' x f) (\text{range } I) ((\text{extChartAt } I x) x) \big).$$$
Lean4
theorem mdifferentiableWithinAt_iff' (f : M → M') (s : Set M) (x : M) :
MDifferentiableWithinAt I I' f s x ↔
ContinuousWithinAt f s x ∧
DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).symm ⁻¹' s ∩ range I)
((extChartAt I x) x) :=
by rw [MDifferentiableWithinAt, liftPropWithinAt_iff']; rfl
