Theorems · Theorem · global analysis

Manifold.IsImmersionAt.map_target_subset_target

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x),
  (⇑h.equiv ∘ fun x_1 => (x_1, 0)) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target

If f is an immersion at x, it maps its domain chart's target to its codomain chart's target: (h.domChart.extend I).target to (h.domChart.extend J).target. Roig and Domingues' [roigdomingues1992] definition of immersions only asks for this inclusion between the targets of the local charts: using mathlib's formalisation conventions, that condition is slightly weaker than source_subset_preimage_source: the latter implies that h.codChart.extend J ∘ f maps h.domChart.source to (h.codChart.extend J).target = (h.codChart.extend I) '' h.codChart.source, but that does not imply f maps h.domChart.source to h.codChart.source; a priori f could map some point f ∘ h.domChart.extend I x ∉ h.codChart.source into the target. Note that this difference only occurs because of our design using junk values; this is not a mathematically meaningful difference. At the same time, this condition is fairly weak: it is implied, for instance, by f being continuous at x (see mk_of_continuousAt), which is easy to ascertain in practice. See target_subset_preimage_target for a version stated using preimages instead of images.

Defined in

Mathlib.Geometry.Manifold.Immersion

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace