IsLocalDiffeomorph.isOpen_range
theorem IsLocalDiffeomorph.isOpen_range :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N}, IsLocalDiffeomorph I J n f → IsOpen (Set.range f)
This theorem states that for a local diffeomorphism, which we denote as `f`, between two differentiable manifolds `M` and `N`, the range of `f` is an open set. The manifolds `M` and `N` are modelled on topological vector spaces `E` and `F` over a nontrivially normed field `𝕜`, respectively. Furthermore, the manifolds `M` and `N` are assumed to have topological spaces `H` and `G` as their chart domains, which are associated via models with corners `I` and `J`. The smoothness class of the diffeomorphism is `n`. The theorem is true for any such local diffeomorphism `f`.
More concisely: For any local diffeomorphism `f` between differentiable manifolds `M` and `N` modelled on topological vector spaces `E` and `F` over a nontrivially normed field `𝕜`, and having chart domains `H` and `G` with associated models of corners `I` and `J`, the range of `f` is an open subset of `N`.
|
IsLocalDiffeomorphOn.isLocalHomeomorphOn
theorem IsLocalDiffeomorphOn.isLocalHomeomorphOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N} {s : Set M}, IsLocalDiffeomorphOn I J n f s → IsLocalHomeomorphOn f s
This theorem asserts that for a given function `f : M → N` defined on a set `s`, if `f` is a local diffeomorphism on `s`, then `f` is also a local homeomorphism on `s`. Here, `M` and `N` are types equipped with topological structures and charted spaces, `𝕜` is a nontrivially normed field, `E` and `F` are normed additive commutative groups equipped with a normed space over `𝕜`, `H` and `G` are topological spaces, and `I` and `J` are models with corners. The notion of a local diffeomorphism involves differentiability, which is a stronger condition than the continuity involved in the notion of a local homeomorphism.
More concisely: If `f : M -> N` is a local diffeomorphism on a set `s` with `M` and `N` being topological spaces and `f` being defined over nontrivially normed fields, then `f` is also a local homeomorphism on `s`.
|
IsLocalDiffeomorphAt.mdifferentiableAt
theorem IsLocalDiffeomorphAt.mdifferentiableAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N} {x : M}, IsLocalDiffeomorphAt I J n f x → 1 ≤ n → MDifferentiableAt I J f x
This theorem states that if a function `f` is a local diffeomorphism at a point `x` in a manifold `M`, then `f` is differentiable at `x`. Here, `M` and `N` are manifolds modeled on the normed vector spaces `E` and `F` over the nontrivially normed field `𝕜`, with corresponding model-with-corners `I` and `J`. The manifold `M` is equipped with topological structures `H` and `G`, and the function `f` has smoothness class `n`, which is greater than or equal to 1. This theorem is applicable in the context of differential geometry and topology.
More concisely: If `f` is a local diffeomorphism of manifolds `M` and `N` at a point `x`, then `f` is differentiable at `x`.
|
Diffeomorph.isLocalDiffeomorph
theorem Diffeomorph.isLocalDiffeomorph :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
(Φ : Diffeomorph I J M N n), IsLocalDiffeomorph I J n ⇑Φ
The theorem `Diffeomorph.isLocalDiffeomorph` states that for any `C^n` diffeomorphism `Φ`, it is also a local diffeomorphism. This is true for any nontrivially normed field `𝕜`, normed additive commutative groups `E` and `F`, topological spaces `H`, `G`, `M`, and `N`, models with corners `I` and `J` based on `𝕜`, `E`, `H`, `F`, and `G`, charted spaces `M` and `N` based on `H` and `G`, and `n` which is a nonnegative integer or infinity. A `C^n` diffeomorphism is a function that is differentiable to any order up to `n` and has an inverse that is also differentiable to any order up to `n`. A local diffeomorphism is a function that is a diffeomorphism when restricted to any point in its domain.
More concisely: A `C^n` diffeomorphism between normed spaces is a local diffeomorphism.
|
IsLocalDiffeomorph.contMDiff
theorem IsLocalDiffeomorph.contMDiff :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N}, IsLocalDiffeomorph I J n f → ContMDiff I J n f
This theorem asserts that if `f`, a function from `M` to `N`, is a `C^n` local diffeomorphism, then it is `C^n` continuously differentiable. Here, `C^n` refers to the property of a function being n-times continuously differentiable. `M` and `N` are types representing differentiable manifolds, with `M` modeled on the normed space `E` over the field `𝕜` with topology `H`, and `N` modeled on the normed space `F` over the same field with topology `G`. The `IsLocalDiffeomorph` predicate captures the property of `f` being a local diffeomorphism (an isomorphism in the category of differentiable manifolds that is local around each point), and `ContMDiff` denotes the property of being continuously differentiable to the degree `n`.
More concisely: If `f` is a `C^n` local diffeomorphism from the differentiable manifolds `M` modeled on the normed space `E` to the differentiable manifold `N` modeled on the normed space `F`, then `f` is `C^n` continuously differentiable.
|
IsLocalDiffeomorphOn.contMDiffOn
theorem IsLocalDiffeomorphOn.contMDiffOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N} {s : Set M}, IsLocalDiffeomorphOn I J n f s → ContMDiffOn I J n f s
The theorem `IsLocalDiffeomorphOn.contMDiffOn` states that if a function `f` is a `C^n` local diffeomorphism on a set `s`, then `f` is continuous and differentiable `n` times (`C^n`) on `s`. This is defined for `f` from a topological space `M` with a charted space structure relative to a model with corners `I` into another topological space `N` with a charted space structure relative to another model with corners `J`. The theorem holds for any types `𝕜`, `E`, `F`, `H`, `G`, `M`, `N`, and `n`, given the appropriate mathematical structures: `𝕜` a non-trivially normed field, `E` and `F` normed additive commutative groups with a normed space structure over `𝕜`, `H` and `G` topological spaces, `M` and `N` topological spaces with charted space structures relative to `I` and `J` respectively, and `n` a non-negative extended natural number (`ℕ∞`).
More concisely: If a function `f : M → N` is a local diffeomorphism of class `C^n` on a set `s ⊆ M`, then `f` is continuous and differentiable `n` times on `s`.
|
IsLocalDiffeomorphAt.contMDiffAt
theorem IsLocalDiffeomorphAt.contMDiffAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N} {x : M}, IsLocalDiffeomorphAt I J n f x → ContMDiffAt I J n f x
The theorem `IsLocalDiffeomorphAt.contMDiffAt` states that if a function `f` from a manifold `M` to a manifold `N` is a `C^n` local diffeomorphism at a point `x` in `M`, then the function `f` is `C^n` differentiable at the point `x`. Here, `C^n` refers to the class of functions that have continuous derivatives up to `n`th order. The manifolds `M` and `N` are assumed to be embedded in Euclidean spaces `E` and `F` respectively, with `I` and `J` serving as the models of these embeddings. The underlying field is denoted by `𝕜`.
More concisely: If a `C^n` function `f` from manifold `M` to manifold `N` is a local diffeomorphism at a point `x` in `M`, then `f` is `C^n` differentiable at `x`.
|
IsLocalDiffeomorphOn.mdifferentiableOn
theorem IsLocalDiffeomorphOn.mdifferentiableOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N} {s : Set M}, IsLocalDiffeomorphOn I J n f s → 1 ≤ n → MDifferentiableOn I J f s
The theorem `IsLocalDiffeomorphOn.mdifferentiableOn` states that, given certain conditions, if a function `f` from `M` to `N` is a local diffeomorphism at the set `s`, then `f` is differentiable at `s`. The conditions include a non-trivial normed field `𝕜`, normed additive commutative group structures on `E`, `F`, `M` and `N`, normed space structures over `𝕜` on `E` and `F`, topological space structures on `H`, `G`, `M` and `N`, charted space structures on `H` and `G` with respective model with corners `I` and `J`, and a natural number or infinity `n` such that `1 ≤ n`.
More concisely: If `f: M -> N` is a local diffeomorphism at `s ∈ M` between Banach spaces `M` and `N` over a normed field `ℝ` with compatible topologies and charted spaces, then `f` is differentiable at `s`.
|
IsLocalDiffeomorph.isLocalHomeomorph
theorem IsLocalDiffeomorph.isLocalHomeomorph :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N}, IsLocalDiffeomorph I J n f → IsLocalHomeomorph f
This theorem states that a local diffeomorphism is a local homeomorphism. In other words, if a function `f` mapping from a manifold `M` to another manifold `N` is a local diffeomorphism, then it is also a local homeomorphism. Here, a local diffeomorphism `f` is a function that is differentiable and its inverse is also differentiable. A local homeomorphism means that for every point in `M`, there exists a homeomorphism from a neighborhood of it to a neighborhood in `N` such that `f` is equivalent to this homeomorphism. The spaces `M` and `N` are modeled on topological spaces `H` and `G`, respectively, which are equipped with models with corners `I` and `J`, and 'smoothness' is defined up to a certain order `n`.
More concisely: A local diffeomorphism between manifolds is a local homeomorphism.
|
IsLocalDiffeomorph.isOpenMap
theorem IsLocalDiffeomorph.isOpenMap :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N}, IsLocalDiffeomorph I J n f → IsOpenMap f
The theorem `IsLocalDiffeomorph.isOpenMap` states that for any given local diffeomorphism `f` from a manifold `M` to another manifold `N`, under certain conditions, `f` is an open map. The conditions being that `M` and `N` are manifolds modeled on the Euclidean spaces `H` and `G` respectively, which in turn are modeled with corners `I` and `J` on the normed vector spaces `E` and `F` over a non-trivially normed field `𝕜`, and `n` is the smoothness class of the diffeomorphism. An open map, in this context, is a function such that the image of any open set in `M` is open in `N`.
More concisely: Given a local diffeomorphism `f: M \to N` between manifolds modeled over Euclidean spaces `E^H` and `E^G`, if `M` and `N` are `n`-smooth, then `f` maps open sets in `M` to open sets in `N`.
|
IsLocalDiffeomorph.mdifferentiable
theorem IsLocalDiffeomorph.mdifferentiable :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : ℕ∞}
{f : M → N}, IsLocalDiffeomorph I J n f → 1 ≤ n → MDifferentiable I J f
The theorem `IsLocalDiffeomorph.mdifferentiable` states that for any nontrivially normed field `𝕜`, normed add commutative groups `E` and `F`, topological spaces `H`, `G`, `M`, and `N`, with `M` and `N` being charted spaces modelled on `H` and `G` respectively, and a map `f` from `M` to `N`, if `f` is a `C^n` local diffeomorphism (which is a function between manifolds that is invertible and both the function and its inverse are `n` times continuously differentiable), then if `n` is greater than or equal to 1, `f` is differentiable. The differentiability is defined with respect to the models with corners `I` and `J` that provide the link between the abstract manifold and the Euclidean space.
More concisely: If `f: M ⟹ N` is a `C^n` local diffeomorphism between charted spaces `M` and `N` over normed fields `𝕜`, `E`, and `F`, then `f` is differentiable when `n ≥ 1`.
|