English
Bundled C^n maps from M to M' are precisely the functions f: M → M' equipped with a proof that f is C^n in the sense of the manifolds I, I'.
Русский
Содержимое C^n-маршрутов между M и M' — это множества функций f: M → M', снабжённые доказательством того, что f гладна класса C^n в смысле структур I, I'.
LaTeX
$$$\operatorname{ContMDiffMap} \; I\; I'\; M\; M'\; n := \{ f: M \to M' \mid \operatorname{ContMDiff} I I' n f \}$$$
Lean4
/-- Bundled `n` times continuously differentiable maps,
denoted as `C^n(I, M; I', M')` and `C^n(I, M; k)` (when the target is a normed space `k` with
the trivial model) in the `Manifold` namespace. -/
def ContMDiffMap :=
{ f : M → M' // ContMDiff I I' n f }
