hasMFDerivAt_id
theorem hasMFDerivAt_id :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
(x : M), HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
The theorem `hasMFDerivAt_id` states that for any nontrivially normed field 𝕜, any normed additive commutative group E, and any normed space over 𝕜 with base E, if we have a topological space H, a model with corners I associated to 𝕜, E and H, a topological space M, a charted space over M with model H, and a smooth manifold with corners based on I and M, then at any point x in M, the manifold derivative at x of the identity map is the identity map on the tangent space at x. This means that the identity map is differentiable at every point on a smooth manifold, and its derivative at any point is just the identity on the tangent space at that point.
More concisely: The identity map on a smooth manifold with corners is differentiable at every point and its derivative is the identity on the tangent space at that point.
|
mdifferentiableAt_id
theorem mdifferentiableAt_id :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{x : M}, MDifferentiableAt I I id x
This theorem states that the identity function is smooth at any point in a smooth manifold. More specifically, for any non-trivially normed field `𝕜`, normed additive commutative group `E`, topological space `H`, and `M` which is a smooth manifold with corners with respect to model with corners `I`, the identity function `id` is continuously differentiable at any point `x` in `M`.
More concisely: The identity function on a smooth manifold is smooth (continuously differentiable).
|
mdifferentiableAt_const
theorem mdifferentiableAt_const :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {x : M} {c : M'},
MDifferentiableAt I I' (fun x => c) x
This theorem states that for any types 𝕜, E, H, M, E', H', and M', where 𝕜 is a non-trivially normed field, E and E' are normed add commutative groups, H, M, H', and M' are topological spaces, with M and M' also charted spaces H and H' respectively, and given the model with corners I for 𝕜, E and H, I' for 𝕜, E' and H', if these satisfy the condition of a smooth manifold with corners, then for any point x in M and constant c in M', the function that maps every point in M to the constant c is differentiable at x.
More concisely: For any smooth manifold with corners (𝕜, E, H, I) and (𝕜, E', H', I'), where 𝕜 is a non-trivially normed field, E and E' are normed add commutative groups, H, H' are topological spaces, and M, M' are charted subspaces of H, H' respectively, the constant function from M to M' is differentiable at every point in M.
|