Theorems · Theorem · manifolds

exists_contMDiff_support_eq_eq_one_iff

∀ {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 t : Set M},
  IsOpen s →
    IsClosed t →
      t ⊆ s →
        ∃ f,
          ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) f ∧
            Set.range f ⊆ Set.Icc 0 1 ∧ Function.support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Given an open set s containing a closed set t in a finite-dimensional real manifold, there exists a smooth function with support equal to s, taking values in [0,1], and equal to 1 exactly on t.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensionalIsManifoldSigmaCompactSpaceT2Space