English
Let f: M → M' be a map between manifolds modeled on (E,H) and (E',H'). Then f is differentiable at every point of M in the manifold sense; that is, for each x ∈ M there exists a derivative df_x: T_x M → T_{f(x)} M' describing the best linear approximation of f at x in tangent spaces.
Русский
Пусть f: M → M' — отображение между мнообразиями, моделируемыми над (E,H) и (E',H'). Тогда f дифференцируема в каждой точке x ∈ M в смысле многообразий; то есть для каждого x существует производная df_x: T_x M → T_{f(x)} M', задающая линейное аппроксимирование f в точке x на касательных пространствах.
LaTeX
$$$\operatorname{MDifferentiable}(I,I')(f) \iff \forall x \in M,\; \exists df_x:\,\mathrm{TangentSpace}(I,x) \to_L[\mathbb{K}] \mathrm{TangentSpace}(I',(f(x)))\text{ such that } HasMFDerivAt(I,I')(f,x,df_x).$$$
Lean4
/-- `MDifferentiable I I' f` indicates that the function `f` between manifolds
has a derivative everywhere.
This is a generalization of `Differentiable` to manifolds. -/
def MDifferentiable (f : M → M') :=
∀ x, MDifferentiableAt I I' f x
