ContMDiffMap.smooth
theorem ContMDiffMap.smooth :
∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
(f : ContMDiffMap I I' M M' ⊤), Smooth I I' ⇑f
This theorem states that for a given continuously differentiable mapping `f` from a manifold `M` to a manifold `M'` (both with possible extra structure), the map is also smooth. The smoothness here refers to the infinite differentiability. The theorem holds in the context of normed additive commutative groups `E` and `E'`, normed spaces over a non-trivially normed field `𝕜`, along with topological spaces `H` and `H'` and their corresponding model with corners `I` and `I'`.
More concisely: A continuously differentiable mapping between manifolds is smooth (infinitely differentiable).
|
ContMDiffMap.ext
theorem ContMDiffMap.ext :
∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : ℕ∞}
{f g : ContMDiffMap I I' M M' n}, (∀ (x : M), f x = g x) → f = g
This theorem states that for any nontrivially normed field `𝕜`, any normed additive commutative groups `E` and `E'`, any topological spaces `H`, `H'`, `M` and `M'`, any model with corners `I` and `I'` over `𝕜`, and any continuously differentiable map `f` and `g` between `M` and `M'` of class `n`, if `f` and `g` are equal at every point in `M`, then `f` and `g` are indeed the same map. In other words, two continuously differentiable maps are equal if they are equal at every point in their domain.
More concisely: For any nontrivially normed field `𝕜`, if two continuously differentiable maps between Banach spaces over `𝕜` are equal at every point, then they are equal.
|