Diffeomorphisms

This file implements diffeomorphisms.

Definitions

• Diffeomorph I I' M M' n: n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'; we do not introduce a separate definition for the case n = ∞; 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 given ModelWithCorners with 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 between M with model I and M with model I.trans_diffeomorph e.

This file also provides diffeomorphisms related to products and disjoint unions.

• Diffeomorph.prodCongr: the product of two diffeomorphisms
• Diffeomorph.prodComm: M × N is diffeomorphic to N × M
• Diffeomorph.prodAssoc: (M × N) × N' is diffeomorphic to M × (N × N')
• Diffeomorph.sumCongr: the disjoint union of two diffeomorphisms
• Diffeomorph.sumComm: M ⊕ M' is diffeomorphic to M' × M
• Diffeomorph.sumAssoc: (M ⊕ N) ⊕ P is diffeomorphic to M ⊕ (N ⊕ P)
• Diffeomorph.sumEmpty: M ⊕ ∅ is diffeomorphic to M

Notations

• M ≃ₘ^n⟮I, I'⟯ M' := Diffeomorph I J M N n
• M ≃ₘ⟮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 : WithTop ℕ∞) extends M ≃ M' : Type (max u_10 u_9)

n-times continuously differentiable diffeomorphism between M and M' with respect to I and I', denoted as M ≃ₘ^n⟮I, I'⟯ M' (in the Manifold namespace).

• 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

def Manifold.«term_≃ₘ^_⟮_,_⟯_» : Lean.TrailingParserDescr

n-times continuously differentiable diffeomorphism between M and M' with respect to I and I', denoted as M ≃ₘ^n⟮I, I'⟯ M' (in the Manifold namespace).

Equations

• One or more equations did not get rendered due to their size.

def Manifold.«term_≃ₘ⟮_,_⟯_» : Lean.TrailingParserDescr

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.

def Manifold.«term_≃ₘ^_[_]_» : Lean.TrailingParserDescr

n-times continuously differentiable diffeomorphism between E and E'.

Equations

• One or more equations did not get rendered due to their size.

def Manifold.«term_≃ₘ[_]_».«delab_app.Diffeomorph» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Manifold.«term_≃ₘ[_]_» : Lean.TrailingParserDescr

Infinitely differentiable diffeomorphism between E and E'.

Equations

• One or more equations did not get rendered due to their size.

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 : WithTop ℕ∞} : Function.Injective 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 : WithTop ℕ∞} : 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 : WithTop ℕ∞} (Φ : Diffeomorph I I' M M' n) : ContMDiffMap I I' M M' n

Interpret a diffeomorphism as a ContMDiffMap.

Equations

• ↑Φ = ⟨⇑Φ, ⋯⟩

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 : WithTop ℕ∞} : 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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) : ContDiff 𝕜 n ⇑h

@[deprecated Diffeomorph.contDiff (since := "2024-11-21")]

theorem Diffeomorph.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : WithTop ℕ∞} (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) : ContDiff 𝕜 n ⇑h

Alias of Diffeomorph.contDiff.

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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} {h h' : Diffeomorph I I' M M' n} : h.toEquiv = h'.toEquiv ↔ h = h'

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 : WithTop ℕ∞} : 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 : WithTop ℕ∞} {h h' : Diffeomorph I I' M M' n} (Heq : ∀ (x : M), h x = h' x) : h = h'

theorem Diffeomorph.ext_iff {𝕜 : 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 : WithTop ℕ∞} {h h' : Diffeomorph I I' M M' n} : h = h' ↔ ∀ (x : M), h x = h' x

instance Diffeomorph.instContinuousMapClassSomeENatTop {𝕜 : 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 : WithTop ℕ∞) : 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 := ⋯ }

@[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 : WithTop ℕ∞) : (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 : WithTop ℕ∞) : ⇑(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 : WithTop ℕ∞} (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 := ⋯ }

@[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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) : ⇑(h₁.trans 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 : WithTop ℕ∞} (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 := ⋯ }

@[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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} : (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set M) : ⇑h '' s = ⇑h.symm ⁻¹' s

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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set N) : ⇑h.symm '' s = ⇑h ⁻¹' s

@[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 : WithTop ℕ∞} {α : Sort u_13} (h : Diffeomorph I J M N n) (f : α → M) : Set.range (⇑h ∘ f) = ⇑h.symm ⁻¹' Set.range f

@[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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set N) : ⇑h '' (⇑h.symm '' s) = s

@[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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set M) : ⇑h.symm '' (⇑h '' s) = s

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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) : M ≃ₜ N

A diffeomorphism is a homeomorphism.

Equations

• h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : N → M'} (hm : m ≤ n) : ContMDiff I I' m (f ∘ ⇑h) ↔ ContMDiff J I' m f

@[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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : M' → M} (hm : m ≤ n) : ContMDiff I' J m (⇑h ∘ f) ↔ ContMDiff I' I m f

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 : WithTop ℕ∞} (h : Diffeomorph I J M N n) (hn : 1 ≤ n) : PartialHomeomorph.MDifferentiable I J h.toHomeomorph.toPartialHomeomorph

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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 := ⋯ }

@[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) {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] : 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 := ⋯ }

@[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) {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] : ↑(I.transDiffeomorph 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) {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] : ↑(I.transDiffeomorph e).symm = ↑I.symm ∘ ⇑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) {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] : Set.range ↑(I.transDiffeomorph 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] {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] (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] {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] (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] {n : WithTop ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) [NeZero n] (x : M) : (extChartAt (I.transDiffeomorph e) x).target = ⇑e.symm ⁻¹' (extChartAt I x).target

instance Diffeomorph.instIsManifoldTransDiffeomorph {𝕜 : 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] {n : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) [IsManifold I n M] : IsManifold (I.transDiffeomorph e) n 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] {n : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) : Diffeomorph I (I.transDiffeomorph e) M M n

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 := ⋯ }

@[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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {f : M' → M} : ContMDiff I' (I.transDiffeomorph e) n f ↔ ContMDiff I' I n f

@[deprecated Diffeomorph.contMDiff_transDiffeomorph_right (since := "2024-11-21")]

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'] {n : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {f : M' → M} : ContMDiff I' (I.transDiffeomorph e) n f ↔ ContMDiff I' I n f

Alias of Diffeomorph.contMDiff_transDiffeomorph_right.

@[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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {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 : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {f : M → M'} : ContMDiff (I.transDiffeomorph e) I' n f ↔ ContMDiff I I' n f

@[deprecated Diffeomorph.contMDiff_transDiffeomorph_left (since := "2024-11-21")]

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'] {n : WithTop ℕ∞} [NeZero n] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) {f : M → M'} : ContMDiff (I.transDiffeomorph e) I' n f ↔ ContMDiff I I' n f

Alias of Diffeomorph.contMDiff_transDiffeomorph_left.

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 : WithTop ℕ∞} (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 := ⋯ }

@[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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) : ⇑(h₁.prodCongr 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 : WithTop ℕ∞) : 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 := ⋯ }

@[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 : WithTop ℕ∞) : (prodComm I J M N n).symm = 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 : WithTop ℕ∞) : ⇑(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 : WithTop ℕ∞) : 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 := ⋯ }

def Diffeomorph.sumCongr {𝕜 : 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] {n : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_15} [TopologicalSpace N] [ChartedSpace H N] {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [TopologicalSpace N'] [ChartedSpace H N'] (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : Diffeomorph I J (M ⊕ M') (N ⊕ N') n

The sum of two diffeomorphisms: this is Sum.map as a diffeomorphism.

Equations

• φ.sumCongr ψ = { toEquiv := φ.sumCongr ψ.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem Diffeomorph.sumCongr_symm_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] {n : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_15} [TopologicalSpace N] [ChartedSpace H N] {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [TopologicalSpace N'] [ChartedSpace H N'] (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : φ.symm.sumCongr ψ.symm = (φ.sumCongr ψ).symm

@[simp]

theorem Diffeomorph.sumCongr_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] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_15} [TopologicalSpace N] [ChartedSpace H N] {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [TopologicalSpace N'] [ChartedSpace H N'] (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : ⇑(φ.sumCongr ψ) = Sum.map ⇑φ ⇑ψ

theorem Diffeomorph.sumCongr_inl {𝕜 : 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] {n : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_15} [TopologicalSpace N] [ChartedSpace H N] {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [TopologicalSpace N'] [ChartedSpace H N'] (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : ⇑(φ.sumCongr ψ) ∘ Sum.inl = Sum.inl ∘ ⇑φ

theorem Diffeomorph.sumCongr_inr {𝕜 : 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] {n : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {N : Type u_15} [TopologicalSpace N] [ChartedSpace H N] {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [TopologicalSpace N'] [ChartedSpace H N'] (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n) : ⇑(φ.sumCongr ψ) ∘ Sum.inr = Sum.inr ∘ ⇑ψ

def Diffeomorph.sumComm {𝕜 : 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 : WithTop ℕ∞) (M' : Type u_13) [TopologicalSpace M'] [ChartedSpace H M'] : Diffeomorph I I (M ⊕ M') (M' ⊕ M) n

The canonical diffeomorphism M ⊕ M' → M' ⊕ M: this is Sum.swap as a diffeomorphism

Equations

• Diffeomorph.sumComm I M n M' = { toEquiv := Equiv.sumComm M M', contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

@[simp]

theorem Diffeomorph.sumComm_coe {𝕜 : 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 : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] : ⇑(sumComm I M n M') = Sum.swap

@[simp]

theorem Diffeomorph.sumComm_symm {𝕜 : 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 : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] : (sumComm I M n M').symm = sumComm I M' n M

theorem Diffeomorph.sumComm_inl {𝕜 : 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 : WithTop ℕ∞) (M' : Type u_13) [TopologicalSpace M'] [ChartedSpace H M'] : ⇑(sumComm I M n M') ∘ Sum.inl = Sum.inr

theorem Diffeomorph.sumComm_inr {𝕜 : 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 : WithTop ℕ∞) (M' : Type u_13) [TopologicalSpace M'] [ChartedSpace H M'] : ⇑(sumComm I M n M') ∘ Sum.inr = Sum.inl

def Diffeomorph.sumAssoc {𝕜 : 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 : WithTop ℕ∞) (M' : Type u_13) [TopologicalSpace M'] [ChartedSpace H M'] (M'' : Type u_14) [TopologicalSpace M''] [ChartedSpace H M''] : Diffeomorph I I ((M ⊕ M') ⊕ M'') (M ⊕ M' ⊕ M'') n

The canonical diffeomorphism (M ⊕ N) ⊕ P → M ⊕ (N ⊕ P)

Equations

• Diffeomorph.sumAssoc I M n M' M'' = { toEquiv := Equiv.sumAssoc M M' M'', contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

@[simp]

theorem Diffeomorph.sumAssoc_coe {𝕜 : 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 : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] {M'' : Type u_14} [TopologicalSpace M''] [ChartedSpace H M''] : ⇑(sumAssoc I M n M' M'') = ⇑(Equiv.sumAssoc M M' M'')

def Diffeomorph.sumEmpty {𝕜 : 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 : WithTop ℕ∞) {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] [IsEmpty M'] : Diffeomorph I I (M ⊕ M') M n

The canonical diffeomorphism M ⊕ ∅ → M

Equations

• Diffeomorph.sumEmpty I M n = { toEquiv := Equiv.sumEmpty M M', contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

@[simp]

theorem Diffeomorph.sumEmpty_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 : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] [IsEmpty M'] : (sumEmpty I M n).toEquiv = Equiv.sumEmpty M M'

@[simp]

theorem Diffeomorph.sumEmpty_apply_inl {𝕜 : 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 : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] [IsEmpty M'] (x : M) : (sumEmpty I M n) (Sum.inl x) = x

def Diffeomorph.empty {𝕜 : 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 : WithTop ℕ∞} {M' : Type u_13} [TopologicalSpace M'] [ChartedSpace H M'] [IsEmpty M] [IsEmpty M'] : Diffeomorph I I M M' n

The unique diffeomorphism between two empty types

Equations

• Diffeomorph.empty = { toEquiv := Equiv.equivOfIsEmpty M M', contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }