Theorems · Definition · global analysis

Manifold.IsSubmersionAtOfComplement.codChart

{𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsSubmersionAtOfComplement F I J n f x →
                                                      OpenPartialHomeomorph N G

A choice of chart on the codomain N of a submersion f at x: w.r.t. this chart and the data h.domChart and h.equiv, f will look like a projection (u, v) ↦ u in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by h.equiv and h.domChart.

Defined in

Mathlib.Geometry.Manifold.Submersion

Cited by

10 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace