contMDiffOn_symm_of_mem_maximalAtlas
theorem contMDiffOn_symm_of_mem_maximalAtlas :
∀ {𝕜 : 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 : PartialHomeomorph M H} {n : ℕ∞},
e ∈ SmoothManifoldWithCorners.maximalAtlas I M → ContMDiffOn I I n (↑e.symm) e.target
This theorem states that for any nontrivially normed field `𝕜`, a normed additive commutative group `E`, a topological space `H`, a model with corners `I` of `𝕜`, `E`, and `H`, a topological space `M`, and a charted space `M` with `H`, if we have a smooth manifold with corners `I` and `M`, and a partial homeomorphism `e` between `M` and `H`, then if `e` is part of the maximal atlas of the smooth manifold, the inverse of `e` is continuously differentiable any number `n` of times on the target of `e`. In more mathematical terms, if `e` is in the maximal atlas of the smooth manifold with corners, then `e` inverse is `C^n` for any `n`.
More concisely: If `e: M ⟶ H` is a partial homeomorphism in the maximal atlas of a smooth manifold with corners `(I, M)`, then `e^(-1)` is continuously differentiable (`C^n`) on `H` for any given natural number `n`.
|
contMDiffOn_of_mem_maximalAtlas
theorem contMDiffOn_of_mem_maximalAtlas :
∀ {𝕜 : 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 : PartialHomeomorph M H} {n : ℕ∞},
e ∈ SmoothManifoldWithCorners.maximalAtlas I M → ContMDiffOn I I n (↑e) e.source
The theorem `contMDiffOn_of_mem_maximalAtlas` states that for any nontrivially normed field `𝕜`, normed add commutative group `E`, topological space `H`, model with corners `I` from `𝕜`, `E` to `H`, topological space `M`, charted space `M` with model `H`, smooth manifold with corners `I` and `M`, partial homeomorphism `e` between `M` and `H`, and natural number or infinity `n`, if `e` is an element of the maximal atlas of the smooth manifold with corners `I` and `M`, then the function represented by `e` is `C^n` continuous and differentiable on the source of `e`. In other words, any member of the maximal atlas of a smooth manifold is `C^n` differentiable for any `n`, where `C^n` is a class of functions which are continuous and have continuous derivatives up to order `n`.
More concisely: If `e` is an element of the maximal atlas of a smooth manifold with corners `I` and `M` over a nontrivially normed field `𝕜`, then `e` is `C^n` continuous and differentiable for any natural number or infinity `n`.
|
isLocalStructomorphOn_contDiffGroupoid_iff
theorem isLocalStructomorphOn_contDiffGroupoid_iff :
∀ {𝕜 : 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]
{M' : Type u_7} [inst_7 : TopologicalSpace M'] [inst_8 : ChartedSpace H M']
[IsM' : SmoothManifoldWithCorners I M'] (f : PartialHomeomorph M M'),
ChartedSpace.LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source ↔
SmoothOn I I (↑f) f.source ∧ SmoothOn I I (↑f.symm) f.target
The theorem `isLocalStructomorphOn_contDiffGroupoid_iff` states that for any two smooth manifolds `M` and `M'` that share the same model-with-corners `I`, a partial homeomorphism `f` from `M` to `M'` is a local structomorphism for `I` if and only if `f` is smoothly differentiable on its domain of definition and its inverse is smoothly differentiable on its range. Here, the differentiability is measured in the sense of the manifold's intrinsic calculus structure given by the model-with-corners `I`.
More concisely: A partial homeomorphism between smooth manifolds with the same model-with-corners is a local structomorphism if and only if it is smoothly differentiable on its domain and its inverse is smoothly differentiable on its range.
|
contMDiffOn_of_mem_contDiffGroupoid
theorem contMDiffOn_of_mem_contDiffGroupoid :
∀ {𝕜 : 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} {n : ℕ∞}
{e' : PartialHomeomorph H H}, e' ∈ contDiffGroupoid ⊤ I → ContMDiffOn I I n (↑e') e'.source
This theorem states that given a nontrivially normed field `𝕜`, a normed add commutative group `E`, a topological space `H`, and a model `I` with corners relating `𝕜`, `E`, and `H`, for any natural number `n` and a partial homeomorphism `e'` in the `contDiffGroupoid ⊤ I`, the function `e'` is continuously differentiable of any order `n` on its source.
More concisely: Given a nontrivially normed field `𝕜`, a normed additive commutative group `E`, a topological space `H`, and a model `I` with corners relating `𝕜`, `E`, and `H`, any partial homeomorphism `e` in the `contDiffGroupoid ⊤ I` is continuously differentiable of order `n` on its source.
|