English
Special case of product with corners: the tangent model is I.prod I, i.e., the tangent bundle model uses a trivial second factor.
Русский
Особый случай произведения моделей с углами: касательная модель равна I.prod I, касательное расслоение моделируется через тривиальный второй фактор.
LaTeX
$$$$ \text{tangent}(I) = I \,.\text{prod } \mathcal{I}(\mathbb{R},E). $$$$
Lean4
/-- Special case of product model with corners, which is trivial on the second factor. This shows up
as the model to tangent bundles. -/
abbrev tangent {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
{H : Type w} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : ModelWithCorners 𝕜 (E × E) (ModelProd H E) :=
I.prod 𝓘(𝕜, E)
