Documentation

Mathlib.Geometry.Manifold.Diffeomorph

Diffeomorphisms #

This file implements diffeomorphisms.

Definitions #

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

Notations #

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).

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.

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.

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

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

Pretty printer defined by notation3 command.

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

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 ℕ∞} :
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
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
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) :
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 ℕ∞} :

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] :
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
@[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 ℕ∞) :
@[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) :
@[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 ℕ∞} :
@[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) :
@[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) :
@[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) :
@[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) :
@[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
@[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) :
@[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) :
@[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) :
@[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 : NM'} {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 : NM'} {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 : NM'} {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 : NM'} (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.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} :
@[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} :
@[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') :

A continuous linear equivalence between normed spaces is a diffeomorphism.

Equations
@[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.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') :
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] :

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] :
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) :
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) :

The identity diffeomorphism between a manifold with model I and the same manifold with model I.trans_diffeomorph e.

Equations
@[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'} :
@[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 : MM'} {x : M} {s : Set M} :
@[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 : MM'} {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 : MM'} {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 : MM'} :
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 : MM'} :
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
@[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
@[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
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
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) :
@[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
@[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
@[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
@[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'] :
@[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