Mathlib Map

Theorems Β· Definition Β· global analysis

Diffeomorph.toContMDiffMap

{π•œ : 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'] β†’
                        {I : ModelWithCorners π•œ E H} β†’
                          {I' : ModelWithCorners π•œ E' H'} β†’
                            {M : Type u_9} β†’
                              [inst_7 : TopologicalSpace M] β†’
                                [inst_8 : ChartedSpace H M] β†’
                                  {M' : Type u_10} β†’
                                    [inst_9 : TopologicalSpace M'] β†’
                                      [inst_10 : ChartedSpace H' M'] β†’
                                        {n : WithTop β„•βˆž} β†’ Diffeomorph I I' M M' n β†’ ContMDiffMap I I' M M' n

Interpret a diffeomorphism as a ContMDiffMap.

Defined in
Mathlib.Geometry.Manifold.Diffeomorph
Cited by
1 results in Mathlib
Foundations
Depth 183 from the axioms Β· uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Diffeomorph.coe_coe Β· cited by 0Diffeomorph.coe_coeDFunLike.coe Β· cited by 62936DFunLike.coeTopologicalSpace Β· cited by 24529TopologicalSpaceNormedAddCommGroup Β· cited by 15752NormedAddCommGroupNormedSpace Β· cited by 12499NormedSpaceNontriviallyNormedField Β· cited by 8742NontriviallyNormedFieldENat Β· cited by 4985ENatWithTop Β· cited by 3754WithTopModelWithCorners Β· cited by 2462ModelWithCornersChartedSpace Β· cited by 2397ChartedSpaceContMDiffMap Β· cited by 125ContMDiffMapDiffeomorph Β· cited by 85DiffeomorphDiffeomorph.contMDiff_toFun Β· cited by 2Diffeomorph.contMDiff_toF…Diffeomorph.toContMDiffMapCITED BYCITES

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.