feat: port Geometry.Manifold.PartitionOfUnity (#5460)

leanprover-community · Jul 6, 2023 · c43889d · c43889d
1 parent 82d6c3a
commit c43889d
Show file tree

Hide file tree

Showing 2 changed files with 597 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1849,6 +1849,7 @@ import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
 import Mathlib.Geometry.Manifold.LocalInvariantProperties
 import Mathlib.Geometry.Manifold.MFDeriv
 import Mathlib.Geometry.Manifold.Metrizable
+import Mathlib.Geometry.Manifold.PartitionOfUnity
 import Mathlib.Geometry.Manifold.Sheaf.Basic
 import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
 import Mathlib.Geometry.Manifold.VectorBundle.Basic