Theorems · Theorem · manifolds

SmoothPartitionOfUnity.exists_isSubordinate

∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M]
  {s : Set M}, IsClosed s → ∀ (U : ι → Set M), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a SmoothPartitionOfUnity ι M s that is subordinate to U.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensionalIsManifoldT2SpaceSigmaCompactSpace