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 M ≃ M' :
Type (max u_10 u_9)
n-times continuously differentiable diffeomorphism between M and M' with respect to I
and I'.
- toFun : M → M'
- invFun : M' → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- contMDiff_toFun : ContMDiff I I' n ⇑self.toEquiv
- contMDiff_invFun : ContMDiff I' I n ⇑self.symm
Instances For
n-times continuously differentiable diffeomorphism between M and M' with respect to I
and I'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Infinitely differentiable diffeomorphism between M and M' with respect to I and I'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
n-times continuously differentiable diffeomorphism between E and E'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Infinitely differentiable diffeomorphism between E and E'.
Equations
- One or more equations did not get rendered due to their size.
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.instEquivLike
{𝕜 : 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'
Equations
- Diffeomorph.instEquivLike = { coe := fun (Φ : Diffeomorph I I' M M' n) => ⇑Φ.toEquiv, inv := fun (Φ : Diffeomorph I I' M M' n) => ⇑Φ.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
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.
Equations
- ↑Φ = ⟨⇑Φ, ⋯⟩
Instances For
instance
Diffeomorph.instCoeContMDiffMap
{𝕜 : 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)
Equations
- Diffeomorph.instCoeContMDiffMap = { coe := Diffeomorph.toContMDiffMap }
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 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 DFunLike.coe
Coercion to function fun 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 h' : Diffeomorph I I' M M' n}
(Heq : ∀ (x : M), h x = h' x)
:
h = h'
instance
Diffeomorph.instContinuousMapClassTopENat
{𝕜 : 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
Equations
- ⋯ = ⋯
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.
Equations
- Diffeomorph.refl I M n = { toEquiv := Equiv.refl M, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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.
Equations
- h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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)
:
h.trans (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.refl I M n).trans 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)
:
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.
Equations
- h.symm = { toEquiv := h.symm, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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)
:
h.trans 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)
:
h.symm.trans 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)
:
(h₁.trans h₂).symm = h₂.symm.trans 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.
Equations
- h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
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)
:
h.toHomeomorph.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)
:
h.symm.toHomeomorph = h.toHomeomorph.symm
@[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)
:
⇑h.toHomeomorph = ⇑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)
:
⇑h.toHomeomorph.symm = ⇑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.toPartialHomeomorph_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)
:
PartialHomeomorph.MDifferentiable I J h.toHomeomorph.toPartialHomeomorph
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 (I.prod J) (I'.prod J') (M × N) (M' × N') n
Product of two diffeomorphisms.
Equations
- h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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)
:
(h₁.prodCongr h₂).symm = h₁.symm.prodCongr 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)
:
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 (I.prod J) (J.prod I) (M × N) (N × M) n
M × N is diffeomorphic to N × M.
Equations
- Diffeomorph.prodComm I J M N n = { toEquiv := Equiv.prodComm M N, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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 ((I.prod J).prod J') (I.prod (J.prod J')) ((M × N) × N') (M × N × N') n
(M × N) × N' is diffeomorphic to M × (N × N').
Equations
- Diffeomorph.prodAssoc I J J' M N N' n = { toEquiv := Equiv.prodAssoc M N N', contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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 : ℕ∞}
(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 : ℕ∞}
(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 : ℕ∞}
(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.
Equations
- e.toDiffeomorph = { toEquiv := e.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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')
:
⇑e.toDiffeomorph = ⇑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')
:
e.symm.toDiffeomorph = e.toDiffeomorph.symm
@[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')
:
⇑e.toDiffeomorph.symm = ⇑e.symm
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.
Equations
- I.transDiffeomorph e = { toPartialEquiv := I.trans e.toPartialEquiv, source_eq := ⋯, uniqueDiffOn' := ⋯, target_subset_closure_interior := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
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' ⊤)
:
@[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' ⊤)
:
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' ⊤)
:
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 (I.transDiffeomorph 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)
:
↑(extChartAt (I.transDiffeomorph e) x).symm = ↑(extChartAt I x).symm ∘ ⇑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 (I.transDiffeomorph 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]
:
SmoothManifoldWithCorners (I.transDiffeomorph e) M
Equations
- ⋯ = ⋯
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 (I.transDiffeomorph e) M M ⊤
The identity diffeomorphism between a manifold with model I and the same manifold
with model I.trans_diffeomorph e.
Equations
- Diffeomorph.toTransDiffeomorph I M e = { toEquiv := Equiv.refl M, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
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' (I.transDiffeomorph 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' (I.transDiffeomorph 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' (I.transDiffeomorph 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}
:
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}
:
@[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 (I.transDiffeomorph 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 (I.transDiffeomorph 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 (I.transDiffeomorph 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'}
:
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'}
: