Theorems · Definition · global analysis

Manifold.IsImmersionAtOfComplement.domChart

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

A choice of chart on the domain M of an immersion f at x: w.r.t. this chart and the data h.codChart and h.equiv, f will look like an inclusion u ↦ (u, 0) in these extended charts. The particular chart is arbitrary, but this choice matches the witnesses given by h.codChart and h.codChart.

Defined in

Mathlib.Geometry.Manifold.Immersion

Cited by

14 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace