Diffeomorphisms #
This file implements diffeomorphisms.
Definitions #
Diffeomorph I I' M M' n:n-times continuously differentiable diffeomorphism betweenMandM'with respect to I and I'; we do not introduce a separate definition for the casen = ∞; we use notation instead.Diffeomorph.toHomeomorph: reinterpret a diffeomorphism as a homeomorphism.ContinuousLinearEquiv.toDiffeomorph: reinterpret a continuous equivalence as a diffeomorphism.ModelWithCorners.transDiffeomorph: compose a givenModelWithCornerswith a diffeomorphism between the old and the new target spaces. Useful, e.g, to turn any finite dimensional manifold into a manifold modelled on a Euclidean space.Diffeomorph.toTransDiffeomorph: the identity diffeomorphism betweenMwith modelIandMwith modelI.trans_diffeomorph e.
Notations #
M ≃ₘ^n⟮I, I'⟯ M':=Diffeomorph I J M N nM ≃ₘ⟮I, I'⟯ M':=Diffeomorph I J M N ⊤E ≃ₘ^n[𝕜] E':=E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'E ≃ₘ[𝕜] E':=E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
Implementation notes #
This notion of diffeomorphism is needed although there is already a notion of 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.
Keywords #
diffeomorphism, manifold
structure
Diffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
(I : ModelWithCorners 𝕜 E H)
(I' : ModelWithCorners 𝕜 E' H')
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(M' : Type u_10)
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
extends
Equiv
:
Type (max u_10 u_9)
- toFun : M → M'
- invFun : M' → M
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- contMDiff_toFun : ContMDiff I I' n ↑s.toEquiv
- contMDiff_invFun : ContMDiff I' I n ↑s.symm
n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'
Instances For
theorem
Diffeomorph.toEquiv_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
:
Function.Injective Diffeomorph.toEquiv
instance
Diffeomorph.instEquivLikeDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
:
EquivLike (Diffeomorph I I' M M' n) M M'
def
Diffeomorph.toContMDiffMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(Φ : Diffeomorph I I' M M' n)
:
ContMDiffMap I I' M M' n
Interpret a diffeomorphism as a ContMDiffMap.
Instances For
instance
Diffeomorph.instCoeDiffeomorphContMDiffMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
:
Coe (Diffeomorph I I' M M' n) (ContMDiffMap I I' M M' n)
theorem
Diffeomorph.continuous
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
:
Continuous ↑h
theorem
Diffeomorph.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
:
ContMDiff I I' n ↑h
theorem
Diffeomorph.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
{x : M}
:
ContMDiffAt I I' n (↑h) x
theorem
Diffeomorph.contMDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
{s : Set M}
{x : M}
:
ContMDiffWithinAt I I' n (↑h) s x
theorem
Diffeomorph.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{n : ℕ∞}
(h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)
:
ContDiff 𝕜 n ↑h
theorem
Diffeomorph.smooth
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
(h : Diffeomorph I I' M M' ⊤)
:
Smooth I I' ↑h
theorem
Diffeomorph.mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
(hn : 1 ≤ n)
:
MDifferentiable I I' ↑h
theorem
Diffeomorph.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
(s : Set M)
(hn : 1 ≤ n)
:
MDifferentiableOn I I' (↑h) s
@[simp]
theorem
Diffeomorph.coe_toEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
:
↑h.toEquiv = ↑h
@[simp]
theorem
Diffeomorph.coe_coe
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
:
↑↑h = ↑h
@[simp]
theorem
Diffeomorph.toEquiv_inj
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
{h : Diffeomorph I I' M M' n}
{h' : Diffeomorph I I' M M' n}
:
theorem
Diffeomorph.coeFn_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
:
Function.Injective FunLike.coe
Coercion to function λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M') is injective.
theorem
Diffeomorph.ext
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
{h : Diffeomorph I I' M M' n}
{h' : Diffeomorph I I' M M' n}
(Heq : ∀ (x : M), ↑h x = ↑h' x)
:
h = h'
instance
Diffeomorph.instContinuousMapClassDiffeomorphTopENatInstENatTop
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
:
ContinuousMapClass (Diffeomorph I J M N ⊤) M N
def
Diffeomorph.refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(n : ℕ∞)
:
Diffeomorph I I M M n
Identity map as a diffeomorphism.
Instances For
@[simp]
theorem
Diffeomorph.refl_toEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(n : ℕ∞)
:
(Diffeomorph.refl I M n).toEquiv = Equiv.refl M
@[simp]
theorem
Diffeomorph.coe_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(n : ℕ∞)
:
↑(Diffeomorph.refl I M n) = id
def
Diffeomorph.trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h₁ : Diffeomorph I I' M M' n)
(h₂ : Diffeomorph I' J M' N n)
:
Diffeomorph I J M N n
Composition of two diffeomorphisms.
Instances For
@[simp]
theorem
Diffeomorph.trans_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
:
Diffeomorph.trans h (Diffeomorph.refl I' M' n) = h
@[simp]
theorem
Diffeomorph.refl_trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(h : Diffeomorph I I' M M' n)
:
Diffeomorph.trans (Diffeomorph.refl I M n) h = h
@[simp]
theorem
Diffeomorph.coe_trans
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h₁ : Diffeomorph I I' M M' n)
(h₂ : Diffeomorph I' J M' N n)
:
↑(Diffeomorph.trans h₁ h₂) = ↑h₂ ∘ ↑h₁
def
Diffeomorph.symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
Diffeomorph J I N M n
Inverse of a diffeomorphism.
Instances For
@[simp]
theorem
Diffeomorph.apply_symm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(x : N)
:
↑h (↑h.symm x) = x
@[simp]
theorem
Diffeomorph.symm_apply_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(x : M)
:
↑h.symm (↑h x) = x
@[simp]
theorem
Diffeomorph.symm_refl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{n : ℕ∞}
:
(Diffeomorph.refl I M n).symm = Diffeomorph.refl I M n
@[simp]
theorem
Diffeomorph.self_trans_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
Diffeomorph.trans h h.symm = Diffeomorph.refl I M n
@[simp]
theorem
Diffeomorph.symm_trans_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
Diffeomorph.trans h.symm h = Diffeomorph.refl J N n
@[simp]
theorem
Diffeomorph.symm_trans'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h₁ : Diffeomorph I I' M M' n)
(h₂ : Diffeomorph I' J M' N n)
:
(Diffeomorph.trans h₁ h₂).symm = Diffeomorph.trans h₂.symm h₁.symm
@[simp]
theorem
Diffeomorph.symm_toEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
h.symm.toEquiv = h.symm
@[simp]
theorem
Diffeomorph.toEquiv_coe_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
↑h.symm = ↑h.symm
theorem
Diffeomorph.image_eq_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(s : Set M)
:
theorem
Diffeomorph.symm_image_eq_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(s : Set N)
:
@[simp]
theorem
Diffeomorph.range_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{α : Sort u_13}
(h : Diffeomorph I J M N n)
(f : α → M)
:
@[simp]
theorem
Diffeomorph.image_symm_image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(s : Set N)
:
@[simp]
theorem
Diffeomorph.symm_image_image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(s : Set M)
:
def
Diffeomorph.toHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
M ≃ₜ N
A diffeomorphism is a homeomorphism.
Instances For
@[simp]
theorem
Diffeomorph.toHomeomorph_toEquiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
(Diffeomorph.toHomeomorph h).toEquiv = h.toEquiv
@[simp]
theorem
Diffeomorph.symm_toHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
@[simp]
theorem
Diffeomorph.coe_toHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
↑(Diffeomorph.toHomeomorph h) = ↑h
@[simp]
theorem
Diffeomorph.coe_toHomeomorph_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
:
↑(Homeomorph.symm (Diffeomorph.toHomeomorph h)) = ↑h.symm
@[simp]
theorem
Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : N → M'}
{s : Set M}
{x : M}
(hm : m ≤ n)
:
ContMDiffWithinAt I I' m (f ∘ ↑h) s x ↔ ContMDiffWithinAt J I' m f (↑h.symm ⁻¹' s) (↑h x)
@[simp]
theorem
Diffeomorph.contMDiffOn_comp_diffeomorph_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : N → M'}
{s : Set M}
(hm : m ≤ n)
:
ContMDiffOn I I' m (f ∘ ↑h) s ↔ ContMDiffOn J I' m f (↑h.symm ⁻¹' s)
@[simp]
theorem
Diffeomorph.contMDiffAt_comp_diffeomorph_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : N → M'}
{x : M}
(hm : m ≤ n)
:
ContMDiffAt I I' m (f ∘ ↑h) x ↔ ContMDiffAt J I' m f (↑h x)
@[simp]
theorem
Diffeomorph.contMDiff_comp_diffeomorph_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : N → M'}
(hm : m ≤ n)
:
@[simp]
theorem
Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : M' → M}
(hm : m ≤ n)
{s : Set M'}
{x : M'}
:
ContMDiffWithinAt I' J m (↑h ∘ f) s x ↔ ContMDiffWithinAt I' I m f s x
@[simp]
theorem
Diffeomorph.contMDiffAt_diffeomorph_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : M' → M}
(hm : m ≤ n)
{x : M'}
:
ContMDiffAt I' J m (↑h ∘ f) x ↔ ContMDiffAt I' I m f x
@[simp]
theorem
Diffeomorph.contMDiffOn_diffeomorph_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : M' → M}
(hm : m ≤ n)
{s : Set M'}
:
ContMDiffOn I' J m (↑h ∘ f) s ↔ ContMDiffOn I' I m f s
@[simp]
theorem
Diffeomorph.contMDiff_diffeomorph_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
{m : ℕ∞}
(h : Diffeomorph I J M N n)
{f : M' → M}
(hm : m ≤ n)
:
theorem
Diffeomorph.toLocalHomeomorph_mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
(h : Diffeomorph I J M N n)
(hn : 1 ≤ n)
:
def
Diffeomorph.prodCongr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{G' : Type u_8}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F G'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{N' : Type u_12}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
(h₁ : Diffeomorph I I' M M' n)
(h₂ : Diffeomorph J J' N N' n)
:
Diffeomorph (ModelWithCorners.prod I J) (ModelWithCorners.prod I' J') (M × N) (M' × N') n
Product of two diffeomorphisms.
Instances For
@[simp]
theorem
Diffeomorph.prodCongr_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{G' : Type u_8}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F G'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{N' : Type u_12}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
(h₁ : Diffeomorph I I' M M' n)
(h₂ : Diffeomorph J J' N N' n)
:
(Diffeomorph.prodCongr h₁ h₂).symm = Diffeomorph.prodCongr h₁.symm h₂.symm
@[simp]
theorem
Diffeomorph.coe_prodCongr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{G : Type u_7}
[TopologicalSpace G]
{G' : Type u_8}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{J : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F G'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{N' : Type u_12}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : ℕ∞}
(h₁ : Diffeomorph I I' M M' n)
(h₂ : Diffeomorph J J' N N' n)
:
↑(Diffeomorph.prodCongr h₁ h₂) = Prod.map ↑h₁ ↑h₂
def
Diffeomorph.prodComm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_11)
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
:
Diffeomorph (ModelWithCorners.prod I J) (ModelWithCorners.prod J I) (M × N) (N × M) n
M × N is diffeomorphic to N × M.
Instances For
@[simp]
theorem
Diffeomorph.prodComm_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_11)
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
:
(Diffeomorph.prodComm I J M N n).symm = Diffeomorph.prodComm J I N M n
@[simp]
theorem
Diffeomorph.coe_prodComm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_11)
[TopologicalSpace N]
[ChartedSpace G N]
(n : ℕ∞)
:
↑(Diffeomorph.prodComm I J M N n) = Prod.swap
def
Diffeomorph.prodAssoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{G' : Type u_8}
[TopologicalSpace G']
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 F G)
(J' : ModelWithCorners 𝕜 F G')
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_11)
[TopologicalSpace N]
[ChartedSpace G N]
(N' : Type u_12)
[TopologicalSpace N']
[ChartedSpace G' N']
(n : ℕ∞)
:
Diffeomorph (ModelWithCorners.prod (ModelWithCorners.prod I J) J')
(ModelWithCorners.prod I (ModelWithCorners.prod J J')) ((M × N) × N') (M × N × N') n
(M × N) × N' is diffeomorphic to M × (N × N').
Instances For
theorem
Diffeomorph.uniqueMDiffOn_image_aux
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners J N]
(h : Diffeomorph I J M N n)
(hn : 1 ≤ n)
{s : Set M}
(hs : UniqueMDiffOn I s)
:
UniqueMDiffOn J (↑h '' s)
@[simp]
theorem
Diffeomorph.uniqueMDiffOn_image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners J N]
(h : Diffeomorph I J M N n)
(hn : 1 ≤ n)
{s : Set M}
:
UniqueMDiffOn J (↑h '' s) ↔ UniqueMDiffOn I s
@[simp]
theorem
Diffeomorph.uniqueMDiffOn_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{G : Type u_7}
[TopologicalSpace G]
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 F G}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace G N]
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners J N]
(h : Diffeomorph I J M N n)
(hn : 1 ≤ n)
{s : Set N}
:
UniqueMDiffOn I (↑h ⁻¹' s) ↔ UniqueMDiffOn J s
@[simp]
theorem
Diffeomorph.uniqueDiffOn_image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n)
(hn : 1 ≤ n)
{s : Set E}
:
UniqueDiffOn 𝕜 (↑h '' s) ↔ UniqueDiffOn 𝕜 s
@[simp]
theorem
Diffeomorph.uniqueDiffOn_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n)
(hn : 1 ≤ n)
{s : Set F}
:
UniqueDiffOn 𝕜 (↑h ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
def
ContinuousLinearEquiv.toDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
:
Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤
A continuous linear equivalence between normed spaces is a diffeomorphism.
Instances For
@[simp]
theorem
ContinuousLinearEquiv.coe_toDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
:
↑(ContinuousLinearEquiv.toDiffeomorph e) = ↑e
@[simp]
theorem
ContinuousLinearEquiv.symm_toDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
:
@[simp]
theorem
ContinuousLinearEquiv.coe_toDiffeomorph_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(e : E ≃L[𝕜] E')
:
↑(ContinuousLinearEquiv.toDiffeomorph e).symm = ↑(ContinuousLinearEquiv.symm e)
def
ModelWithCorners.transDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
:
ModelWithCorners 𝕜 E' H
Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.
Instances For
@[simp]
theorem
ModelWithCorners.coe_transDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
:
↑(ModelWithCorners.transDiffeomorph I e) = ↑e ∘ ↑I
@[simp]
theorem
ModelWithCorners.coe_transDiffeomorph_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
:
↑(ModelWithCorners.symm (ModelWithCorners.transDiffeomorph I e)) = ↑(ModelWithCorners.symm I) ∘ ↑e.symm
theorem
ModelWithCorners.transDiffeomorph_range
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
:
Set.range ↑(ModelWithCorners.transDiffeomorph I e) = ↑e '' Set.range ↑I
theorem
ModelWithCorners.coe_extChartAt_transDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
(x : M)
:
↑(extChartAt (ModelWithCorners.transDiffeomorph I e) x) = ↑e ∘ ↑(extChartAt I x)
theorem
ModelWithCorners.coe_extChartAt_transDiffeomorph_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
(x : M)
:
↑(LocalEquiv.symm (extChartAt (ModelWithCorners.transDiffeomorph I e) x)) = ↑(LocalEquiv.symm (extChartAt I x)) ∘ ↑e.symm
theorem
ModelWithCorners.extChartAt_transDiffeomorph_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ⊤)
(x : M)
:
(extChartAt (ModelWithCorners.transDiffeomorph I e) x).target = ↑e.symm ⁻¹' (extChartAt I x).target
instance
Diffeomorph.smoothManifoldWithCorners_transDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
[SmoothManifoldWithCorners I M]
:
def
Diffeomorph.toTransDiffeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_9)
[TopologicalSpace M]
[ChartedSpace H M]
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
:
Diffeomorph I (ModelWithCorners.transDiffeomorph I e) M M ⊤
The identity diffeomorphism between a manifold with model I and the same manifold
with model I.trans_diffeomorph e.
Instances For
@[simp]
theorem
Diffeomorph.contMDiffWithinAt_transDiffeomorph_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M' → M}
{x : M'}
{s : Set M'}
:
ContMDiffWithinAt I' (ModelWithCorners.transDiffeomorph I e) n f s x ↔ ContMDiffWithinAt I' I n f s x
@[simp]
theorem
Diffeomorph.contMDiffAt_transDiffeomorph_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M' → M}
{x : M'}
:
ContMDiffAt I' (ModelWithCorners.transDiffeomorph I e) n f x ↔ ContMDiffAt I' I n f x
@[simp]
theorem
Diffeomorph.contMDiffOn_transDiffeomorph_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M' → M}
{s : Set M'}
:
ContMDiffOn I' (ModelWithCorners.transDiffeomorph I e) n f s ↔ ContMDiffOn I' I n f s
@[simp]
theorem
Diffeomorph.contMDiff_transDiffeomorph_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M' → M}
:
ContMDiff I' (ModelWithCorners.transDiffeomorph I e) n f ↔ ContMDiff I' I n f
theorem
Diffeomorph.smooth_transDiffeomorph_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M' → M}
:
Smooth I' (ModelWithCorners.transDiffeomorph I e) f ↔ Smooth I' I f
@[simp]
theorem
Diffeomorph.contMDiffWithinAt_transDiffeomorph_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M → M'}
{x : M}
{s : Set M}
:
ContMDiffWithinAt (ModelWithCorners.transDiffeomorph I e) I' n f s x ↔ ContMDiffWithinAt I I' n f s x
@[simp]
theorem
Diffeomorph.contMDiffAt_transDiffeomorph_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M → M'}
{x : M}
:
ContMDiffAt (ModelWithCorners.transDiffeomorph I e) I' n f x ↔ ContMDiffAt I I' n f x
@[simp]
theorem
Diffeomorph.contMDiffOn_transDiffeomorph_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M → M'}
{s : Set M}
:
ContMDiffOn (ModelWithCorners.transDiffeomorph I e) I' n f s ↔ ContMDiffOn I I' n f s
@[simp]
theorem
Diffeomorph.contMDiff_transDiffeomorph_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M → M'}
:
ContMDiff (ModelWithCorners.transDiffeomorph I e) I' n f ↔ ContMDiff I I' n f
theorem
Diffeomorph.smooth_transDiffeomorph_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{H : Type u_5}
[TopologicalSpace H]
{H' : Type u_6}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_10}
[TopologicalSpace M']
[ChartedSpace H' M']
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ⊤)
{f : M → M'}
:
Smooth (ModelWithCorners.transDiffeomorph I e) I' f ↔ Smooth I I' f