Documentation

Mathlib.Geometry.Manifold.Diffeomorph

Diffeomorphisms #

This file implements diffeomorphisms.

Definitions #

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 : ℕ∞) extends Equiv :
Type (max u_10 u_9)

n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'

Instances For
    theorem Diffeomorph.toEquiv_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
    Function.Injective Diffeomorph.toEquiv
    instance Diffeomorph.instEquivLikeDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
    EquivLike (Diffeomorph I I' M M' n) M M'
    def Diffeomorph.toContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (Φ : Diffeomorph I I' M M' n) :
    ContMDiffMap I I' M M' n

    Interpret a diffeomorphism as a ContMDiffMap.

    Instances For
      instance Diffeomorph.instCoeDiffeomorphContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
      Coe (Diffeomorph I I' M M' n) (ContMDiffMap I I' M M' n)
      theorem Diffeomorph.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
      theorem Diffeomorph.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
      ContMDiff I I' n h
      theorem Diffeomorph.contMDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) {x : M} :
      ContMDiffAt I I' n (h) x
      theorem Diffeomorph.contMDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) {s : Set M} {x : M} :
      ContMDiffWithinAt I I' n (h) s x
      theorem Diffeomorph.contDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {n : ℕ∞} (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n) :
      ContDiff 𝕜 n h
      theorem Diffeomorph.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] (h : Diffeomorph I I' M M' ) :
      Smooth I I' h
      theorem Diffeomorph.mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) (hn : 1 n) :
      MDifferentiable I I' h
      theorem Diffeomorph.mdifferentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) (s : Set M) (hn : 1 n) :
      MDifferentiableOn I I' (h) s
      @[simp]
      theorem Diffeomorph.coe_toEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
      h.toEquiv = h
      @[simp]
      theorem Diffeomorph.coe_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
      h = h
      @[simp]
      theorem Diffeomorph.toEquiv_inj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} {h : Diffeomorph I I' M M' n} {h' : Diffeomorph I I' M M' n} :
      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 : ℕ∞} :
      Function.Injective FunLike.coe

      Coercion to function λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M') is injective.

      theorem Diffeomorph.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} {h : Diffeomorph I I' M M' n} {h' : Diffeomorph I I' M M' n} (Heq : ∀ (x : M), h x = h' x) :
      h = h'
      def Diffeomorph.refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (n : ℕ∞) :
      Diffeomorph I I M M n

      Identity map as a diffeomorphism.

      Instances For
        @[simp]
        theorem Diffeomorph.refl_toEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (n : ℕ∞) :
        (Diffeomorph.refl I M n).toEquiv = Equiv.refl M
        @[simp]
        theorem Diffeomorph.coe_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (n : ℕ∞) :
        ↑(Diffeomorph.refl I M n) = id
        def Diffeomorph.trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
        Diffeomorph I J M N n

        Composition of two diffeomorphisms.

        Instances For
          @[simp]
          theorem Diffeomorph.trans_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
          @[simp]
          theorem Diffeomorph.refl_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
          @[simp]
          theorem Diffeomorph.coe_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
          ↑(Diffeomorph.trans h₁ h₂) = h₂ h₁
          def Diffeomorph.symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
          Diffeomorph J I N M n

          Inverse of a diffeomorphism.

          Instances For
            @[simp]
            theorem Diffeomorph.apply_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) (x : N) :
            h (h.symm x) = x
            @[simp]
            theorem Diffeomorph.symm_apply_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) (x : M) :
            h.symm (h x) = x
            @[simp]
            theorem Diffeomorph.symm_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {n : ℕ∞} :
            @[simp]
            theorem Diffeomorph.self_trans_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
            @[simp]
            theorem Diffeomorph.symm_trans_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
            @[simp]
            theorem Diffeomorph.symm_trans' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
            (Diffeomorph.trans h₁ h₂).symm = Diffeomorph.trans h₂.symm h₁.symm
            @[simp]
            theorem Diffeomorph.symm_toEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
            h.symm.toEquiv = h.symm
            @[simp]
            theorem Diffeomorph.toEquiv_coe_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
            h.symm = h.symm
            theorem Diffeomorph.image_eq_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) (s : Set M) :
            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 : ℕ∞} (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 : ℕ∞} {α : 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 : ℕ∞} (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 : ℕ∞} (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 : ℕ∞} (h : Diffeomorph I J M N n) :
            M ≃ₜ N

            A diffeomorphism is a homeomorphism.

            Instances For
              @[simp]
              theorem Diffeomorph.toHomeomorph_toEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
              (Diffeomorph.toHomeomorph h).toEquiv = h.toEquiv
              @[simp]
              theorem Diffeomorph.symm_toHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
              @[simp]
              theorem Diffeomorph.coe_toHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
              @[simp]
              theorem Diffeomorph.coe_toHomeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
              @[simp]
              theorem Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : 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 : ℕ∞} (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 : ℕ∞} (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 : ℕ∞} (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 : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) {s : Set M'} {x : M'} :
              ContMDiffWithinAt I' J m (h f) s x ContMDiffWithinAt I' I m f s x
              @[simp]
              theorem Diffeomorph.contMDiffAt_diffeomorph_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) {x : M'} :
              ContMDiffAt I' J m (h f) x ContMDiffAt I' I m f x
              @[simp]
              theorem Diffeomorph.contMDiffOn_diffeomorph_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) {s : Set M'} :
              ContMDiffOn I' J m (h f) s ContMDiffOn I' I m f s
              @[simp]
              theorem Diffeomorph.contMDiff_diffeomorph_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) :
              ContMDiff I' J m (h f) ContMDiff I' I m f
              def Diffeomorph.prodCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :

              Product of two diffeomorphisms.

              Instances For
                @[simp]
                theorem Diffeomorph.prodCongr_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
                (Diffeomorph.prodCongr h₁ h₂).symm = Diffeomorph.prodCongr h₁.symm h₂.symm
                @[simp]
                theorem Diffeomorph.coe_prodCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
                ↑(Diffeomorph.prodCongr h₁ h₂) = Prod.map h₁ h₂
                def Diffeomorph.prodComm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) :

                M × N is diffeomorphic to N × M.

                Instances For
                  @[simp]
                  theorem Diffeomorph.prodComm_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) :
                  (Diffeomorph.prodComm I J M N n).symm = Diffeomorph.prodComm J I N M n
                  @[simp]
                  theorem Diffeomorph.coe_prodComm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞) :
                  ↑(Diffeomorph.prodComm I J M N n) = Prod.swap
                  def Diffeomorph.prodAssoc {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G) (J' : ModelWithCorners 𝕜 F G') (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (N' : Type u_12) [TopologicalSpace N'] [ChartedSpace G' N'] (n : ℕ∞) :

                  (M × N) × N' is diffeomorphic to M × (N × N').

                  Instances For
                    theorem Diffeomorph.uniqueMDiffOn_image_aux {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners J N] (h : Diffeomorph I J M N n) (hn : 1 n) {s : Set M} (hs : UniqueMDiffOn I s) :
                    UniqueMDiffOn J (h '' s)
                    @[simp]
                    theorem Diffeomorph.uniqueMDiffOn_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners J N] (h : Diffeomorph I J M N n) (hn : 1 n) {s : Set M} :
                    @[simp]
                    theorem Diffeomorph.uniqueMDiffOn_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners J N] (h : Diffeomorph I J M N n) (hn : 1 n) {s : Set N} :
                    @[simp]
                    theorem Diffeomorph.uniqueDiffOn_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) (hn : 1 n) {s : Set E} :
                    UniqueDiffOn 𝕜 (h '' s) UniqueDiffOn 𝕜 s
                    @[simp]
                    theorem Diffeomorph.uniqueDiffOn_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} (h : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) (hn : 1 n) {s : Set F} :
                    UniqueDiffOn 𝕜 (h ⁻¹' s) UniqueDiffOn 𝕜 s
                    def ContinuousLinearEquiv.toDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :

                    A continuous linear equivalence between normed spaces is a diffeomorphism.

                    Instances For
                      @[simp]
                      theorem ContinuousLinearEquiv.coe_toDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
                      def ModelWithCorners.transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) :

                      Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.

                      Instances For
                        @[simp]
                        theorem ModelWithCorners.coe_transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) :
                        theorem ModelWithCorners.extChartAt_transDiffeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) (x : M) :
                        (extChartAt (ModelWithCorners.transDiffeomorph I e) x).target = e.symm ⁻¹' (extChartAt I x).target

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

                        Instances For
                          @[simp]
                          theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : M'M} {x : M'} {s : Set M'} :
                          @[simp]
                          theorem Diffeomorph.contMDiffAt_transDiffeomorph_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : M'M} {x : M'} :
                          @[simp]
                          theorem Diffeomorph.contMDiffOn_transDiffeomorph_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : M'M} {s : Set M'} :
                          @[simp]
                          theorem Diffeomorph.contMDiff_transDiffeomorph_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : M'M} :
                          theorem Diffeomorph.smooth_transDiffeomorph_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : M'M} :
                          @[simp]
                          theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : 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 : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : MM'} {x : M} :
                          @[simp]
                          theorem Diffeomorph.contMDiffOn_transDiffeomorph_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : MM'} {s : Set M} :
                          @[simp]
                          theorem Diffeomorph.contMDiff_transDiffeomorph_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : MM'} :
                          theorem Diffeomorph.smooth_transDiffeomorph_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) {f : MM'} :