English
For a model with corners I on E, the range of I has a unique MDiffOn structure; in particular, the standard model with corners induces a global differentiability property on its range.
Русский
Для модели с краями I на E пределы имеют уникальную MDiffOn-структуру; в частности, стандартная модель с краями порождает глобальную дифференцируемость на диапазоне.
LaTeX
$$$\text{ModelWithCorners.uniqueMDiffOn}(I) :\; \mathrm{UniqueMDiffOn}(\mathcal{I}_{𝕜,E}, \mathrm{range}(I)).$$$
Lean4
/-- The derivative, as a map between the tangent bundles -/
def tangentMap (f : M → M') : TangentBundle I M → TangentBundle I' M' := fun p =>
⟨f p.1, (mfderiv I I' f p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
