Commit 2023-07-03 06:01 ea71ff14

View on Github →

feat: port Geometry.Manifold.WhitneyEmbedding (#5666)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/WhitneyEmbedding.lean

added theorem SmoothBumpCovering.comp_embeddingPiTangent_mfderiv

added def SmoothBumpCovering.embeddingPiTangent

added theorem SmoothBumpCovering.embeddingPiTangent_coe

added theorem SmoothBumpCovering.embeddingPiTangent_injOn

added theorem SmoothBumpCovering.embeddingPiTangent_injective

added theorem SmoothBumpCovering.embeddingPiTangent_injective_mfderiv

added theorem SmoothBumpCovering.embeddingPiTangent_ker_mfderiv

added theorem SmoothBumpCovering.exists_immersion_euclidean

added theorem exists_embedding_euclidean_of_compact