Diffeomorph.coeFn_injective
theorem Diffeomorph.coeFn_injective :
∀ {𝕜 : 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_5} [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{n : ℕ∞}, Function.Injective DFunLike.coe
The theorem `Diffeomorph.coeFn_injective` states that the coercion to function operation, represented by `DFunLike.coe`, is injective for diffeomorphisms. In other words, given two diffeomorphisms `h` and `h'` of type `M ≃ₘ^n⟮I, I'⟯ M'` (smooth diffeomorphisms between manifolds `M` and `M'` with smoothness class `n` and with model with corners `I` and `I'`), if the functions obtained by coercing `h` and `h'` to the type `(h : M → M')` are the same, then `h` and `h'` were originally the same diffeomorphism. This theorem holds for all types and instances satisfying the conditions in the theorem: nontrivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, normed spaces over `𝕜` for `E` and `E'`, topological spaces `H` and `H'`, model with corners `I` and `I'`, charted spaces `M` and `M'` with structures of topological spaces, and a natural number `n` or infinity (∞).
More concisely: The coercion to function operation for smooth diffeomorphisms between manifolds is injective, that is, if two diffeomorphisms have the same function representation when coerced to the type `(h : M → M')`, then they are equal as diffeomorphisms.
|
Diffeomorph.continuous
theorem Diffeomorph.continuous :
∀ {𝕜 : 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_5} [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{n : ℕ∞} (h : Diffeomorph I I' M M' n), Continuous ⇑h
This theorem states that for any nontrivially normed field 𝕜, normed additive commutative groups E and E', normed spaces over 𝕜 E and E', topological spaces H and H', models with corners I and I' for 𝕜 with respect to E and H, and I' for 𝕜 with respect to E' and H', topological spaces M and M', charted spaces M and M' with respect to H and H' respectively, and for any natural number or infinity (ℕ∞) n, if there exists a diffeomorphism h between I and I' which maps M to M' with smoothness level n, then the diffeomorphism h is continuous. In other words, a diffeomorphism that maps between two topological spaces is always a continuous function.
More concisely: For any nontrivially normed fields 𝕜, normed additive commutative groups E and E', topological spaces H and H', and charted spaces M and M' over 𝕜 with respect to H and H' respectively, if there exists a diffeomorphism h between the models of 𝕜 in E and H, and h maps M to M' with smoothness level n, then h is continuous.
|