Theorems · Inductive type · manifolds

SmoothBumpCovering

Type uι →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            ModelWithCorners ℝ E H →
              (M : Type uM) →
                [inst_3 : TopologicalSpace M] →
                  [ChartedSpace H M] → [FiniteDimensional ℝ E] → optParam (Set M) Set.univ → Type (max uM uι)

We say that a collection of SmoothBumpFunctions is a SmoothBumpCovering of a set s if * (f i).c ∈ s for all i; * the family fun i ↦ support (f i) is locally finite; * for each point x ∈ s there exists i such that f i =ᶠ[𝓝 x] 1; in other words, x belongs to the interior of {y | f i y = 1}; If M is a finite-dimensional real manifold which is a σ-compact Hausdorff topological space, then for every covering U : M → Set M, ∀ x, U x ∈ 𝓝 x, there exists a SmoothBumpCovering subordinate to U, see SmoothBumpCovering.exists_isSubordinate. This covering can be used, e.g., to construct a partition of unity and to prove the weak Whitney embedding theorem.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

32 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensional