Theorems · Theorem · manifolds

SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source_of_isClosed

∀ {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 → ∃ f, f.IsSubordinate fun x => (chartAt H ↑x).source

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensionalIsManifoldT2SpaceSigmaCompactSpace