Theorems · Theorem · global analysis

Manifold.IsImmersionAt.mk_of_continuousAt

∀ {𝕜 : 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},
  ContinuousAt f x →
    ∀ (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
      x ∈ domChart.source →
        f x ∈ codChart.source →
          domChart ∈ IsManifold.maximalAtlas I n M →
            codChart ∈ IsManifold.maximalAtlas J n N →
              Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x => (x, 0))
                  (domChart.extend I).target →
                Manifold.IsImmersionAt I J n f x

f : M → N is a C^n immersion at x if there are charts φ and ψ of M and N around x and f x, respectively such that in these charts, f looks like u ↦ (u, 0). This version does not assume that f maps φ.source to ψ.source, but that f is continuous at x.

Defined in

Mathlib.Geometry.Manifold.Immersion

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace