Theorems · Theorem · manifolds

IsOpen.exists_contMDiff_support_eq

∀ {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] [SigmaCompactSpace M] [T2Space M] {n : ℕ∞} {s : Set M},
  IsOpen s → ∃ f, Function.support f = s ∧ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) f ∧ ∀ (x : M), 0 ≤ f x

Given an open set in a finite-dimensional real manifold, there exists a nonnegative smooth function with support equal to s.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensionalIsManifoldSigmaCompactSpaceT2Space