Local diffeomorphisms between manifolds #
In this file, we define C^n local diffeomorphisms between manifolds.
A C^n map f : M → N is a local diffeomorphism at x iff there are neighbourhoods s
and t of x and f x, respectively such that f restricts to a diffeomorphism
between s and t. f is called a local diffeomorphism on s iff it is a local diffeomorphism
at every x ∈ s, and a local diffeomorphism iff it is a local diffeomorphism on univ.
Main definitions #
IsLocalDiffeomorphAt I J n f x:fis aC^nlocal diffeomorphism atxIsLocalDiffeomorphOn I J n f s:fis aC^nlocal diffeomorphism onsIsLocalDiffeomorph I J n f:fis aC^nlocal diffeomorphism
Main results #
Each of
Diffeomorph,IsLocalDiffeomorph,IsLocalDiffeomorphOnandIsLocalDiffeomorphAtimplies the next condition.IsLocalDiffeomorph.isLocalHomeomorph: a local diffeomorphisms is a local homeomorphism, similarly for local diffeomorphism onsIsLocalDiffeomorph.isOpen_range: the image of a local diffeomorphism is openIslocalDiffeomorph.diffeomorph_of_bijective: a bijective local diffeomorphism is a diffeomorphismDiffeomorph.mfderivToContinuousLinearEquiv: each differential of aC^ndiffeomorphism (n ≥ 1) is a linear equivalence.LocalDiffeomorphAt.mfderivToContinuousLinearEquiv: iffis a local diffeomorphism atx, the differentialmfderiv I J n f xis a continuous linear equivalence.LocalDiffeomorph.mfderivToContinuousLinearEquiv: iffis a local diffeomorphism, each differentialmfderiv I J n f xis a continuous linear equivalence.
TODO #
- an injective local diffeomorphism is a diffeomorphism to its image
- if
fisC^natxandmfderiv I J n f xis a linear isomorphism,fis a local diffeomorphism atx(using the inverse function theorem).
Implementation notes #
This notion of diffeomorphism is needed although there is already a notion of local structomorphism
because structomorphisms do not allow the model spaces H and H' of the two manifolds to be
different, i.e. for a structomorphism one has to impose H = H' which is often not the case in
practice.
Tags #
local diffeomorphism, manifold
structure
PartialDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_7)
[TopologicalSpace N]
[ChartedSpace G N]
(n : WithTop ℕ∞)
extends PartialEquiv M N :
Type (max u_6 u_7)
A partial diffeomorphism on s is a function f : M → N such that f restricts to a
diffeomorphism s → t between open subsets of M and N, respectively.
This is an auxiliary definition and should not be used outside of this file.
- toFun : M → N
- invFun : N → M
- contMDiffOn_toFun : ContMDiffOn I J n (↑self.toPartialEquiv) self.source
- contMDiffOn_invFun : ContMDiffOn J I n self.invFun self.target
Instances For
instance
instCoeFunPartialDiffeomorphForall
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_7)
[TopologicalSpace N]
[ChartedSpace G N]
(n : WithTop ℕ∞)
:
CoeFun (PartialDiffeomorph I J M N n) fun (x : PartialDiffeomorph I J M N n) => M → N
Coercion of a PartialDiffeomorph to function.
Note that a PartialDiffeomorph is not DFunLike (like PartialHomeomorph),
as toFun doesn't determine invFun outside of target.
Equations
- instCoeFunPartialDiffeomorphForall I J M N n = { coe := fun (Φ : PartialDiffeomorph I J M N n) => ↑Φ.toPartialEquiv }
def
Diffeomorph.toPartialDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(h : Diffeomorph I J M N n)
:
PartialDiffeomorph I J M N n
A diffeomorphism is a partial diffeomorphism.
Equations
- h.toPartialDiffeomorph = { toPartialEquiv := h.toHomeomorph.toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }
Instances For
def
PartialDiffeomorph.toPartialHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
:
A partial diffeomorphism is also a local homeomorphism.
Equations
- Φ.toPartialHomeomorph = { toPartialEquiv := Φ.toPartialEquiv, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
Instances For
def
PartialDiffeomorph.symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
:
PartialDiffeomorph J I N M n
The inverse of a local diffeomorphism.
Equations
Instances For
theorem
PartialDiffeomorph.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
:
ContMDiffOn I J n (↑Φ.toPartialEquiv) Φ.source
theorem
PartialDiffeomorph.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
(hn : 1 ≤ n)
:
MDifferentiableOn I J (↑Φ.toPartialEquiv) Φ.source
theorem
PartialDiffeomorph.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : PartialDiffeomorph I J M N n)
(hn : 1 ≤ n)
{x : M}
(hx : x ∈ Φ.source)
:
MDifferentiableAt I J (↑Φ.toPartialEquiv) x
def
IsLocalDiffeomorphAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : WithTop ℕ∞)
(f : M → N)
(x : M)
:
f : M → N is called a C^n local diffeomorphism at x iff there exist
open sets U ∋ x and V ∋ f x and a diffeomorphism Φ : U → V such that f = Φ on U.
Equations
- IsLocalDiffeomorphAt I J n f x = ∃ (Φ : PartialDiffeomorph I J M N n), x ∈ Φ.source ∧ Set.EqOn f (↑Φ.toPartialEquiv) Φ.source
Instances For
theorem
PartialDiffeomorph.isLocalDiffeomorphAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : WithTop ℕ∞)
(φ : PartialDiffeomorph I J M N n)
{x : M}
(hx : x ∈ φ.source)
:
IsLocalDiffeomorphAt I J n (↑φ.toPartialEquiv) x
noncomputable def
IsLocalDiffeomorphAt.localInverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
PartialDiffeomorph J I N M n
An arbitrary choice of local inverse of f near x.
Equations
- hf.localInverse = (Classical.choose hf).symm
Instances For
theorem
IsLocalDiffeomorphAt.localInverse_open_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
theorem
IsLocalDiffeomorphAt.localInverse_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
theorem
IsLocalDiffeomorphAt.localInverse_mem_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
theorem
IsLocalDiffeomorphAt.contmdiffOn_localInverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv) hf.localInverse.source
theorem
IsLocalDiffeomorphAt.localInverse_right_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
{y : N}
(hy : y ∈ hf.localInverse.source)
:
theorem
IsLocalDiffeomorphAt.localInverse_eqOn_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
Set.EqOn (f ∘ ↑hf.localInverse.toPartialEquiv) id hf.localInverse.source
theorem
IsLocalDiffeomorphAt.localInverse_eventuallyEq_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
theorem
IsLocalDiffeomorphAt.localInverse_left_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
{x' : M}
(hx' : x' ∈ hf.localInverse.target)
:
theorem
IsLocalDiffeomorphAt.localInverse_eqOn_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
Set.EqOn (↑hf.localInverse.toPartialEquiv ∘ f) id hf.localInverse.target
theorem
IsLocalDiffeomorphAt.localInverse_eventuallyEq_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
theorem
IsLocalDiffeomorphAt.localInverse_isLocalDiffeomorphAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
IsLocalDiffeomorphAt J I n (↑hf.localInverse.toPartialEquiv) (f x)
theorem
IsLocalDiffeomorphAt.localInverse_contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv) hf.localInverse.source
theorem
IsLocalDiffeomorphAt.localInverse_contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
ContMDiffAt J I n (↑hf.localInverse.toPartialEquiv) (f x)
theorem
IsLocalDiffeomorphAt.localInverse_mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
(hn : 1 ≤ n)
:
MDifferentiableAt J I (↑hf.localInverse.toPartialEquiv) (f x)
def
IsLocalDiffeomorphOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : WithTop ℕ∞)
(f : M → N)
(s : Set M)
:
f : M → N is called a C^n local diffeomorphism on s iff it is a local diffeomorphism
at each x : s.
Equations
- IsLocalDiffeomorphOn I J n f s = ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x
Instances For
def
IsLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
(n : WithTop ℕ∞)
(f : M → N)
:
f : M → N is a C^n local diffeomorphism iff it is a local diffeomorphism
at each x ∈ M.
Equations
- IsLocalDiffeomorph I J n f = ∀ (x : M), IsLocalDiffeomorphAt I J n f x
Instances For
theorem
isLocalDiffeomorphOn_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(s : Set M)
:
theorem
isLocalDiffeomorph_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
:
theorem
isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
:
theorem
IsLocalDiffeomorph.isLocalDiffeomorphOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(s : Set M)
:
IsLocalDiffeomorphOn I J n f s
Basic properties of local diffeomorphisms #
theorem
IsLocalDiffeomorphAt.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
:
ContMDiffAt I J n f x
A C^n local diffeomorphism at x is C^n differentiable at x.
theorem
IsLocalDiffeomorphAt.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
(hn : 1 ≤ n)
:
MDifferentiableAt I J f x
A local diffeomorphism at x is differentiable at x.
theorem
IsLocalDiffeomorphOn.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{s : Set M}
(hf : IsLocalDiffeomorphOn I J n f s)
:
ContMDiffOn I J n f s
A C^n local diffeomorphism on s is C^n on s.
theorem
IsLocalDiffeomorphOn.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{s : Set M}
(hf : IsLocalDiffeomorphOn I J n f s)
(hn : 1 ≤ n)
:
MDifferentiableOn I J f s
A local diffeomorphism on s is differentiable on s.
theorem
IsLocalDiffeomorph.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
ContMDiff I J n f
A C^n local diffeomorphism is C^n.
theorem
IsLocalDiffeomorph.mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hn : 1 ≤ n)
:
MDifferentiable I J f
A C^n local diffeomorphism is differentiable.
theorem
Diffeomorph.isLocalDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I J M N n)
:
IsLocalDiffeomorph I J n ⇑Φ
A C^n diffeomorphism is a local diffeomorphism.
theorem
IsLocalDiffeomorphOn.isLocalHomeomorphOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{s : Set M}
(hf : IsLocalDiffeomorphOn I J n f s)
:
A local diffeomorphism on s is a local homeomorphism on s.
theorem
IsLocalDiffeomorph.isLocalHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
A local diffeomorphism is a local homeomorphism.
theorem
IsLocalDiffeomorph.isOpenMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
A local diffeomorphism is an open map.
theorem
IsLocalDiffeomorph.isOpen_range
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
A local diffeomorphism has open range.
def
IsLocalDiffeomorph.image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
The image of a local diffeomorphism is open.
Instances For
theorem
IsLocalDiffeomorph.image_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
:
noncomputable def
IsLocalDiffeomorph.diffeomorph_of_bijective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hf' : Function.Bijective f)
:
Diffeomorph I J M N n
A bijective local diffeomorphism is a diffeomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated IsLocalDiffeomorph.diffeomorph_of_bijective (since := "2025-03-24")]
def
IslocalDiffeomorph.diffeomorph_of_bijective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hf' : Function.Bijective f)
:
Diffeomorph I J M N n
Alias of IsLocalDiffeomorph.diffeomorph_of_bijective.
A bijective local diffeomorphism is a diffeomorphism.
Equations
Instances For
noncomputable def
IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
(hn : 1 ≤ n)
:
If f is a C^n local diffeomorphism at x, for n ≥ 1, the differential df_x
is a linear equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
(hn : 1 ≤ n)
:
noncomputable def
Diffeomorph.mfderivToContinuousLinearEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I J M N n)
(hn : 1 ≤ n)
(x : M)
:
Each differential of a C^n diffeomorphism of Banach manifolds (n ≥ 1)
is a linear equivalence.
Equations
Instances For
theorem
Diffeomorph.mfderivToContinuousLinearEquiv_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{x : M}
(Φ : Diffeomorph I J M N n)
(hn : 1 ≤ n)
:
noncomputable def
IsLocalDiffeomorph.mfderivToContinuousLinearEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hn : 1 ≤ n)
(x : M)
:
If f is a C^n local diffeomorphism of Banach manifolds (n ≥ 1),
each differential is a linear equivalence.
Equations
Instances For
theorem
IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_4}
[TopologicalSpace H]
{G : Type u_5}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
{f : M → N}
(hf : IsLocalDiffeomorph I J n f)
(hn : 1 ≤ n)
(x : M)
: