Theorems · Theorem · global analysis

SmoothBumpCovering.exists_immersion_euclidean

∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] {H : Type uH}
  [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {ι : Type u_1} [Finite ι]
  (f : SmoothBumpCovering ι I M),
  ∃ n e,
    ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧
      Function.Injective e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)

Baby version of the Whitney weak embedding theorem: if M admits a finite covering by supports of bump functions, then for some n it can be immersed into the n-dimensional Euclidean space.

Defined in

Mathlib.Geometry.Manifold.WhitneyEmbedding

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldT2SpaceFinite