English
The tangent space at each point carries the structure of a real normed space, inherited from the ambient vector space.
Русский
Каждое касательное пространство на точке является вещественным нормированным пространством, полученным из окружающего пространства.
LaTeX
$$$$TangentSpace(\\mathcal{I}(\\mathbb{R},F))\\text{ carries a }\\mathbb{R}\\text{-normed space structure with the same norm as in }F.$$$$
Lean4
/-- Register on the tangent space to a normed vector space the same `NormedSpace` 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 normedSpaceTangentSpaceVectorSpace (x : E) : NormedSpace ℝ (TangentSpace 𝓘(ℝ, E) x) :=
inferInstanceAs (NormedSpace ℝ E)
