57 Manifolds and cell complexes

TheoremWhitney embedding theorem#

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 embedded into the n-dimensional Euclidean space.

exists_embedding_euclidean_of_compact.{uE, uH, uM} {E : Type uE} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M]
  [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M] :
  ∃ n e,
    ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧
      Topology.IsClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)

baby version: for compact manifolds; embedding into some n.

Sources

• Mathlib documentation: exists_embedding_euclidean_of_compact
• Source of exists_embedding_euclidean_of_compact in Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
• 1000+ theorems list: Q1306095
• 1000+ theorems project: Q1306095
• Wikipedia: Whitney embedding theorem
• Wikidata: Q1306095

Mathlibexists_embedding_euclidean_of_compact

Uses 22

Statement usesCompactness in terms of filters · Finite-dimensionality · Hausdorff space · Induced topology · Inner product space, over \(R\) or \(C\) · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\) · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners)

Proof usesBasis · Cardinal · Closure · Completeness of R · Differentiable function between normed vector spaces · Equivalence of norms in finite dimension · Kernel of a linear map · Linear independence · Metric structure · Noetherian module · Noetherian ring · Product of vector spaces · Sum of subspaces · Topological ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.