Theorems · Theorem · manifolds

Metric.exists_contMDiffMap_forall_closedBall_subset

∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] {n : ℕ∞} {M : Type u_1}
  [inst_4 : MetricSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] {K U : ι → Set M},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i

Let M be a smooth σ-compact manifold with a metric. Let K : ι → Set M be a locally finite family of closed sets, let U : ι → Set M be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive smooth function δ : M → ℝ≥0 such that for any i and x ∈ K i, we have Metric.closedBall x (δ x) ⊆ U i.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceFiniteDimensionalMetricSpaceChartedSpaceIsManifoldSigmaCompactSpace