English
The tangent space at any point x of the manifold M is the space E, i.e., T_x M ≅ E.
Русский
Граница касательной пространства в любой точке x многообразия M есть пространство E, то есть T_x M ≅ E.
LaTeX
$$TangentSpace(I,x) ≅ E$$
Lean4
/-- The tangent space at a point of the manifold `M`. It is just `E`. We could use instead
`(tangentBundleCore I M).toFiberBundleCore.fiber x`, but we use `E` to help the kernel.
The definition of `TangentSpace` is not reducible so that type class inference
does not pick wrong instances.
-/
@[nolint unusedArguments]
def TangentSpace {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
{H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
(_x : M) : Type u :=
E
deriving TopologicalSpace, AddCommGroup, IsTopologicalAddGroup, Module 𝕜, ContinuousSMul 𝕜,
-- the following instance derives from the previous one, but through an instance with priority 100
-- which takes a long time to be found. We register a shortcut instance instead
ContinuousConstSMul 𝕜
