Theorems · Definition · manifolds

SmoothBumpCovering.IsSubordinate

{ι : Type uι} →
  {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} → SmoothBumpCovering ι I M s → (M → Set M) → Prop

We say that f : SmoothBumpCovering ι I M s is subordinate to a map U : M → Set M if for each index i, we have tsupport (f i) ⊆ U (f i).c. This notion is a bit more general than being subordinate to an open covering of M, because we make no assumption about the way U x depends on x.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensional