English
If f is MDifferentiableAt, then f is continuous at x.
Русский
Если f дифференцируема в точке, то она непрерывна в этой точке.
LaTeX
$$$\text{MDifferentiableAt } I I' f x \Rightarrow \text{ContinuousAt } f x$$$
Lean4
/-- `MDifferentiableAt I I' f x` indicates that the function `f` between manifolds
has a derivative at the point `x`.
This is a generalization of `DifferentiableAt` to manifolds.
We require continuity in the definition, as otherwise points close to `x` could be sent by
`f` outside of the chart domain around `f x`. Then the chart could do anything to the image points,
and in particular by coincidence `writtenInExtChartAt I I' x f` could be differentiable, while
this would not mean anything relevant. -/
def MDifferentiableAt (f : M → M') (x : M) :=
LiftPropAt (DifferentiableWithinAtProp I I') f x
