Theorems · Inductive type · global analysis

Diffeomorph

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E' H' →
                            (M : Type u_9) →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H M] →
                                  (M' : Type u_10) →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → WithTop ℕ∞ → Type (max u_10 u_9)

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

Defined in

Mathlib.Geometry.Manifold.Diffeomorph

Cited by

85 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace