normedAddCommGroupTangentSpaceVectorSpace

English

There is a canonical NormedAddCommGroup structure on each tangent space of the model with corners Real F.

Русский

На каждом касательном пространстве касательной модели с углами Real F задана каноническая структура NormedAddCommGroup.

LaTeX

$$$$\\text{normedAddCommGroup on }TangentSpace(\\mathcal{I}(\\mathbb{R},F))_x.$$$$

Lean4

/-- Register on the tangent space to a normed vector space the same `NormedAddCommGroup` structure
as in the vector space.

Should not be a global instance, as it does not coincide definitionally with the Riemannian
structure for inner product spaces, but can be activated locally. -/
def normedAddCommGroupTangentSpaceVectorSpace (x : E) : NormedAddCommGroup (TangentSpace 𝓘(ℝ, E) x) :=
  inferInstanceAs (NormedAddCommGroup E)

Похожие утверждения