Theorems · Theorem · manifolds

exists_contMDiffMap_forall_mem_convex_of_local

∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM}
  [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M]
  [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞},
  (∀ (x : M), Convex ℝ (t x)) →
    (∀ (x : M), ∃ U ∈ nhds x, ∃ g, ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y) →
      ∃ g, ∀ (x : M), g x ∈ t x

Let M be a σ-compact Hausdorff finite-dimensional topological manifold. Let t : M → Set F be a family of convex sets. Suppose that for each point x : M there exists a neighborhood U ∈ 𝓝 x and a function g : M → F such that g is $C^n$ smooth on U and g y ∈ t y for all y ∈ U. Then there exists a $C^n$ smooth function g : C^n⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. This is a special case of exists_contMDiffSection_forall_mem_convex_of_local where V is the trivial bundle. See also exists_contMDiffMap_mem_convex_of_local_const.

Defined in

Mathlib.Geometry.Manifold.PartitionOfUnity

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiniteDimensionalIsManifoldSigmaCompactSpaceT2Space