SmoothMap.coe_one
theorem SmoothMap.coe_one :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
{H : Type u_4} [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5}
[inst_6 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N]
[inst_8 : ChartedSpace H N] {G : Type u_10} [inst_9 : One G] [inst_10 : TopologicalSpace G]
[inst_11 : ChartedSpace H' G], ⇑1 = 1
This theorem asserts that in the context of smooth maps, for any non-trivially normed field 𝕜, normed add commutative groups E and E', normed spaces over 𝕜 E and E', topological spaces H, H', N and G, model with corners I and I', charted space H N and charted space H' G, and given one operation in G, the coercion of the multiplicative identity (one) to a function is equal to the identity function.
More concisely: In the context of smooth maps and non-trivially normed fields, the coercion of the multiplicative identity to a function equals the identity function for any group operations in charted spaces over the fields.
|
SmoothMap.coe_zero
theorem SmoothMap.coe_zero :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
{H : Type u_4} [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5}
[inst_6 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N]
[inst_8 : ChartedSpace H N] {G : Type u_10} [inst_9 : Zero G] [inst_10 : TopologicalSpace G]
[inst_11 : ChartedSpace H' G], ⇑0 = 0
This theorem states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, topological spaces `H`, `H'`, `N`, and `G`, a model with corners `I` on `E`, `H`, another model with corners `I'` on `E'`, `H'`, a charted space structure on `N` and `G`, and given that `G` is a zero type, the function application of zero equals zero. This result is valid in the context of smooth manifolds with corners, which are generalizations of smooth manifolds and used in the field of differential geometry.
More concisely: Given a non-trivially normed field, normed additive commutative groups, topological spaces, model with corners on these objects, a charted space structure on two zero-type spaces, the function application of zero equals zero. (This theorem holds in the context of smooth manifolds with corners.)
|