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.contMDiff_toFun {𝕜 : 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 : ℕ∞} (self : Diffeomorph I I' M M' n) :
    ContMDiff I I' n self.toEquiv
    theorem Diffeomorph.contMDiff_invFun {𝕜 : 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 : ℕ∞} (self : Diffeomorph I I' M M' n) :
    ContMDiff I' I n self.symm

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

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

      Infinitely differentiable diffeomorphism between M and M' with respect to I and I'.

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

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

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

          Infinitely differentiable diffeomorphism between E and E'.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Diffeomorph.toEquiv_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
            Function.Injective Diffeomorph.toEquiv
            instance Diffeomorph.instEquivLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
            EquivLike (Diffeomorph I I' M M' n) M M'
            Equations
            • Diffeomorph.instEquivLike = { coe := fun (Φ : Diffeomorph I I' M M' n) => Φ.toEquiv, inv := fun (Φ : Diffeomorph I I' M M' n) => Φ.symm, left_inv := , right_inv := , coe_injective' := }
            def Diffeomorph.toContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (Φ : Diffeomorph I I' M M' n) :
            ContMDiffMap I I' M M' n

            Interpret a diffeomorphism as a ContMDiffMap.

            Equations
            • Φ = Φ,
            Instances For
              instance Diffeomorph.instCoeContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} :
              Coe (Diffeomorph I I' M M' n) (ContMDiffMap I I' M M' n)
              Equations
              • Diffeomorph.instCoeContMDiffMap = { coe := Diffeomorph.toContMDiffMap }
              theorem Diffeomorph.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
              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 DFunLike.coe

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

              theorem Diffeomorph.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} {h : Diffeomorph I I' M M' n} {h' : Diffeomorph I I' M M' n} (Heq : ∀ (x : M), h x = h' x) :
              h = h'
              instance Diffeomorph.instContinuousMapClassTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] :
              Equations
              • =
              def Diffeomorph.refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (n : ℕ∞) :
              Diffeomorph I I M M n

              Identity map as a diffeomorphism.

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

                Composition of two diffeomorphisms.

                Equations
                • h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, contMDiff_toFun := , contMDiff_invFun := }
                Instances For
                  @[simp]
                  theorem Diffeomorph.trans_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
                  h.trans (Diffeomorph.refl I' M' n) = h
                  @[simp]
                  theorem Diffeomorph.refl_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
                  (Diffeomorph.refl I M n).trans h = h
                  @[simp]
                  theorem Diffeomorph.coe_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
                  (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 : ℕ∞} (h : Diffeomorph I J M N n) :
                  Diffeomorph J I N M n

                  Inverse of a diffeomorphism.

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

                    Equations
                    • h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := , continuous_invFun := }
                    Instances For
                      @[simp]
                      theorem Diffeomorph.toHomeomorph_toEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
                      h.toHomeomorph.toEquiv = h.toEquiv
                      @[simp]
                      theorem Diffeomorph.symm_toHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
                      h.symm.toHomeomorph = h.toHomeomorph.symm
                      @[simp]
                      theorem Diffeomorph.coe_toHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
                      h.toHomeomorph = h
                      @[simp]
                      theorem Diffeomorph.coe_toHomeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) :
                      h.toHomeomorph.symm = h.symm
                      @[simp]
                      theorem Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : 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
                      theorem Diffeomorph.toPartialHomeomorph_mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_7} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (h : Diffeomorph I J M N n) (hn : 1 n) :
                      PartialHomeomorph.MDifferentiable I J h.toHomeomorph.toPartialHomeomorph
                      def Diffeomorph.prodCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
                      Diffeomorph (I.prod J) (I'.prod J') (M × N) (M' × N') n

                      Product of two diffeomorphisms.

                      Equations
                      • h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, contMDiff_toFun := , contMDiff_invFun := }
                      Instances For
                        @[simp]
                        theorem Diffeomorph.prodCongr_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
                        (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
                        @[simp]
                        theorem Diffeomorph.coe_prodCongr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {H' : Type u_6} [TopologicalSpace H'] {G : Type u_7} [TopologicalSpace G] {G' : Type u_8} [TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_10} [TopologicalSpace M'] [ChartedSpace H' M'] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {N' : Type u_12} [TopologicalSpace N'] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
                        (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 : ℕ∞) :
                        Diffeomorph (I.prod J) (J.prod I) (M × N) (N × M) n

                        M × N is diffeomorphic to N × M.

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

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

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

                            Equations
                            • e.toDiffeomorph = { toEquiv := e.toEquiv, contMDiff_toFun := , contMDiff_invFun := }
                            Instances For
                              @[simp]
                              theorem ContinuousLinearEquiv.coe_toDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
                              e.toDiffeomorph = e
                              @[simp]
                              theorem ContinuousLinearEquiv.symm_toDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
                              e.symm.toDiffeomorph = e.toDiffeomorph.symm
                              @[simp]
                              theorem ContinuousLinearEquiv.coe_toDiffeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
                              e.toDiffeomorph.symm = e.symm
                              def ModelWithCorners.transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) :

                              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 := , unique_diff' := , continuous_toFun := , continuous_invFun := }
                              Instances For
                                @[simp]
                                theorem ModelWithCorners.coe_transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) :
                                (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) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) :
                                (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) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) :
                                Set.range (I.transDiffeomorph e) = e '' Set.range I
                                theorem ModelWithCorners.coe_extChartAt_transDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) (x : M) :
                                (extChartAt (I.transDiffeomorph e) x) = e (extChartAt I x)
                                theorem ModelWithCorners.coe_extChartAt_transDiffeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) (x : M) :
                                (extChartAt (I.transDiffeomorph e) x).symm = (extChartAt I x).symm e.symm
                                theorem ModelWithCorners.extChartAt_transDiffeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' ) (x : M) :
                                (extChartAt (I.transDiffeomorph e) x).target = e.symm ⁻¹' (extChartAt I x).target
                                Equations
                                • =
                                def Diffeomorph.toTransDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9) [TopologicalSpace M] [ChartedSpace H M] (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F ) :
                                Diffeomorph I (I.transDiffeomorph e) M M

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

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