Theorems · Theorem · manifolds

SmoothBumpCovering.exists_isSubordinate

∀ {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]
  [inst_5 : FiniteDimensional ℝ E] {s : Set M} {U : M → Set M} [T2Space M] [SigmaCompactSpace M],
  IsClosed s → (∀ x ∈ s, U x ∈ nhds x) → ∃ ι f, f.IsSubordinate U

Let M be a smooth manifold modelled on a finite-dimensional real vector space. Suppose also that M is a Hausdorff σ-compact topological space. Let s be a closed set in M and U : M → Set M be a collection of sets such that U x ∈ 𝓝 x for every x ∈ s. Then there exists a smooth bump covering of s that is subordinate to U.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensionalT2SpaceSigmaCompactSpace