# mathlibdocumentation

geometry.manifold.partition_of_unity

# Smooth partition of unity #

In this file we define two structures, smooth_bump_covering and smooth_partition_of_unity. Both structures describe coverings of a set by a locally finite family of supports of smooth functions with some additional properties. The former structure is mostly useful as an intermediate step in the construction of a smooth partition of unity but some proofs that traditionally deal with a partition of unity can use a smooth_bump_covering as well.

Given a real manifold M and its subset s, a smooth_bump_covering ι I M s is a collection of smooth_bump_functions f i indexed by i : ι such that

• the center of each f i belongs to s;

• the family of sets support (f i) is locally finite;

• for each x ∈ s, there exists i : ι such that f i =ᶠ[𝓝 x] 1. In the same settings, a smooth_partition_of_unity ι I M s is a collection of smooth nonnegative functions f i : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, i : ι, such that

• the family of sets support (f i) is locally finite;

• for each x ∈ s, the sum ∑ᶠ i, f i x equals one;

• for each x, the sum ∑ᶠ i, f i x is less than or equal to one.

We say that f : smooth_bump_covering ι 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.

We prove that on a smooth finitely dimensional real manifold with σ-compact Hausdorff topology, for any U : M → set M such that ∀ x ∈ s, U x ∈ 𝓝 x there exists a smooth_bump_covering ι I M s subordinate to U. Then we use this fact to prove a similar statement about smooth partitions of unity, see smooth_partition_of_unity.exists_is_subordinate.

Finally, we use existence of a partition of unity to prove lemma exists_smooth_forall_mem_convex_of_local that allows us to construct a globally defined smooth function from local functions.

## TODO #

• Build a framework for to transfer local definitions to global using partition of unity and use it to define, e.g., the integral of a differential form over a manifold. Lemma exists_smooth_forall_mem_convex_of_local is a first step in this direction.

## Tags #

smooth bump function, partition of unity

### Covering by supports of smooth bump functions #

In this section we define smooth_bump_covering ι I M s to be a collection of smooth_bump_functions such that their supports is a locally finite family of sets and for each x ∈ s some function f i from the collection is equal to 1 in a neighborhood of x. A covering of this type is useful to construct a smooth partition of unity and can be used instead of a partition of unity in some proofs.

We prove that on a smooth finite dimensional real manifold with σ-compact Hausdorff topology, for any U : M → set M such that ∀ x ∈ s, U x ∈ 𝓝 x there exists a smooth_bump_covering ι I M s subordinate to U. Then we use this fact to prove a version of the Whitney embedding theorem: any compact real manifold can be embedded into ℝ^n for large enough n.

@[nolint]
structure smooth_bump_covering (ι : Type uι) {E : Type uE} [ E] {H : Type uH} (I : H) (M : Type uM) [ M] (s : set M := set.univ) :
Type (max uM uι)

We say that a collection of smooth_bump_functions is a smooth_bump_covering of a set s if

• (f i).c ∈ s for all i;
• the family λ 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 smooth_bump_covering subordinate to U, see smooth_bump_covering.exists_is_subordinate.

This covering can be used, e.g., to construct a partition of unity and to prove the weak Whitney embedding theorem.

Instances for smooth_bump_covering
structure smooth_partition_of_unity (ι : Type uι) {E : Type uE} [ E] {H : Type uH} (I : H) (M : Type uM) [ M] (s : set M := set.univ) :
Type (max uM uι)

We say that that a collection of functions form a smooth partition of unity on a set s if

• all functions are infinitely smooth and nonnegative;
• the family λ i, support (f i) is locally finite;
• for all x ∈ s the sum ∑ᶠ i, f i x equals one;
• for all x, the sum ∑ᶠ i, f i x is less than or equal to one.
Instances for smooth_partition_of_unity
@[protected, instance]
def smooth_partition_of_unity.has_coe_to_fun {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} :
has_coe_to_fun s) (λ (_x : s), ι → )
Equations
@[protected]
theorem smooth_partition_of_unity.locally_finite {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) :
theorem smooth_partition_of_unity.nonneg {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (i : ι) (x : M) :
0 (f i) x
theorem smooth_partition_of_unity.sum_eq_one {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) {x : M} (hx : x s) :
finsum (λ (i : ι), (f i) x) = 1
theorem smooth_partition_of_unity.sum_le_one {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (x : M) :
finsum (λ (i : ι), (f i) x) 1
noncomputable def smooth_partition_of_unity.to_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) :
s

Reinterpret a smooth partition of unity as a continuous partition of unity.

Equations
theorem smooth_partition_of_unity.smooth_sum {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) :
(λ (x : M), finsum (λ (i : ι), (f i) x))
theorem smooth_partition_of_unity.le_one {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (i : ι) (x : M) :
(f i) x 1
theorem smooth_partition_of_unity.sum_nonneg {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (x : M) :
0 finsum (λ (i : ι), (f i) x)
theorem smooth_partition_of_unity.cont_mdiff_smul {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) {n : ℕ∞} {g : M → F} {i : ι} (hg : ∀ (x : M), x tsupport (f i) g x) :
n (λ (x : M), (f i) x g x)
theorem smooth_partition_of_unity.smooth_smul {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) {g : M → F} {i : ι} (hg : ∀ (x : M), x tsupport (f i) g x) :
(λ (x : M), (f i) x g x)
theorem smooth_partition_of_unity.cont_mdiff_finsum_smul {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) {n : ℕ∞} {g : ι → M → F} (hg : ∀ (i : ι) (x : M), x tsupport (f i) (g i) x) :
n (λ (x : M), finsum (λ (i : ι), (f i) x g i x))

If f is a smooth partition of unity on a set s : set M and g : ι → M → F is a family of functions such that g i is $C^n$ smooth at every point of the topological support of f i, then the sum λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem smooth_partition_of_unity.smooth_finsum_smul {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) {g : ι → M → F} (hg : ∀ (i : ι) (x : M), x tsupport (f i) (g i) x) :
(λ (x : M), finsum (λ (i : ι), (f i) x g i x))

If f is a smooth partition of unity on a set s : set M and g : ι → M → F is a family of functions such that g i is smooth at every point of the topological support of f i, then the sum λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem smooth_partition_of_unity.finsum_smul_mem_convex {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) {g : ι → M → F} {t : set F} {x : M} (hx : x s) (hg : ∀ (i : ι), (f i) x 0g i x t) (ht : t) :
finsum (λ (i : ι), (f i) x g i x) t
def smooth_partition_of_unity.is_subordinate {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (U : ι → set M) :
Prop

A smooth partition of unity f i is subordinate to a family of sets U i indexed by the same type if for each i the closure of the support of f i is a subset of U i.

Equations
@[simp]
theorem smooth_partition_of_unity.is_subordinate_to_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} {f : s} {U : ι → set M} :
theorem smooth_partition_of_unity.is_subordinate.to_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} {f : s} {U : ι → set M} :

Alias of the reverse direction of smooth_partition_of_unity.is_subordinate_to_partition_of_unity.

theorem smooth_partition_of_unity.is_subordinate.cont_mdiff_finsum_smul {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} {f : s} {n : ℕ∞} {U : ι → set M} {g : ι → M → F} (hf : f.is_subordinate U) (ho : ∀ (i : ι), is_open (U i)) (hg : ∀ (i : ι), (g i) (U i)) :
n (λ (x : M), finsum (λ (i : ι), (f i) x g i x))

If f is a smooth partition of unity on a set s : set M subordinate to a family of open sets U : ι → set M and g : ι → M → F is a family of functions such that g i is $C^n$ smooth on U i, then the sum λ x, ∑ᶠ i, f i x • g i x is $C^n$ smooth on the whole manifold.

theorem smooth_partition_of_unity.is_subordinate.smooth_finsum_smul {ι : Type uι} {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} {f : s} {U : ι → set M} {g : ι → M → F} (hf : f.is_subordinate U) (ho : ∀ (i : ι), is_open (U i)) (hg : ∀ (i : ι), (g i) (U i)) :
(λ (x : M), finsum (λ (i : ι), (f i) x g i x))

If f is a smooth partition of unity on a set s : set M subordinate to a family of open sets U : ι → set M and g : ι → M → F is a family of functions such that g i is smooth on U i, then the sum λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem bump_covering.smooth_to_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (hf : ∀ (i : ι), (f i)) (i : ι) :
noncomputable def bump_covering.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (hf : ∀ (i : ι), (f i)) :
s

A bump_covering such that all functions in this covering are smooth generates a smooth partition of unity.

In our formalization, not every f : bump_covering ι M s with smooth functions f i is a smooth_bump_covering; instead, a smooth_bump_covering is a covering by supports of smooth_bump_functions. So, we define bump_covering.to_smooth_partition_of_unity, then reuse it in smooth_bump_covering.to_smooth_partition_of_unity.

Equations
@[simp]
theorem bump_covering.to_smooth_partition_of_unity_to_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (hf : ∀ (i : ι), (f i)) :
@[simp]
theorem bump_covering.coe_to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : s) (hf : ∀ (i : ι), (f i)) (i : ι) :
theorem bump_covering.is_subordinate.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} {f : s} {U : ι → set M} (h : f.is_subordinate U) (hf : ∀ (i : ι), (f i)) :
@[protected, instance]
def smooth_bump_covering.has_coe_to_fun {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} :
has_coe_to_fun M s) (λ (x : M s), Π (i : ι), (x.c i))
Equations
@[simp]
theorem smooth_bump_covering.coe_mk {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (c : ι → M) (to_fun : Π (i : ι), (c i)) (h₁ : ∀ (i : ι), c i s) (h₂ : locally_finite (λ (i : ι), function.support (to_fun i))) (h₃ : ∀ (x : M), x s(∃ (i : ι), (to_fun i) =ᶠ[nhds x] 1)) :
{c := c, to_fun := to_fun, c_mem' := h₁, locally_finite' := h₂, eventually_eq_one' := h₃} = to_fun
def smooth_bump_covering.is_subordinate {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (f : M s) (U : M → set M) :
Prop

We say that f : smooth_bump_covering ι 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.

Equations
theorem smooth_bump_covering.is_subordinate.support_subset {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} {fs : M s} {U : M → set M} (h : fs.is_subordinate U) (i : ι) :
function.support (fs i) U (fs.c i)
theorem smooth_bump_covering.exists_is_subordinate {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] {s : set M} {U : M → set M} [t2_space M] (hs : is_closed s) (hU : ∀ (x : M), x sU x nhds x) :
∃ (ι : Type uM) (f : M s),

Let M be a smooth manifold with corners modelled on a finite dimensional real vector space. Suppose also that M is a Hausdorff σ-compact topological space. Let s be a closed set in M and U : M → set M be a collection of sets such that U x ∈ 𝓝 x for every x ∈ s. Then there exists a smooth bump covering of s that is subordinate to U.

@[protected]
theorem smooth_bump_covering.locally_finite {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) :
@[protected]
theorem smooth_bump_covering.point_finite {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) :
{i : ι | (fs i) x 0}.finite
theorem smooth_bump_covering.mem_chart_at_source_of_eq_one {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) {i : ι} {x : M} (h : (fs i) x = 1) :
theorem smooth_bump_covering.mem_ext_chart_at_source_of_eq_one {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) {i : ι} {x : M} (h : (fs i) x = 1) :
x (fs.c i)).source
noncomputable def smooth_bump_covering.ind {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) (hx : x s) :
ι

Index of a bump function such that fs i =ᶠ[𝓝 x] 1.

Equations
theorem smooth_bump_covering.eventually_eq_one {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) (hx : x s) :
(fs (fs.ind x hx)) =ᶠ[nhds x] 1
theorem smooth_bump_covering.apply_ind {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) (hx : x s) :
(fs (fs.ind x hx)) x = 1
theorem smooth_bump_covering.mem_support_ind {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) (hx : x s) :
x function.support (fs (fs.ind x hx))
theorem smooth_bump_covering.mem_chart_at_ind_source {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) (hx : x s) :
x (fs.c (fs.ind x hx))).to_local_equiv.source
theorem smooth_bump_covering.mem_ext_chart_at_ind_source {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) (x : M) (hx : x s) :
x (fs.c (fs.ind x hx))).source
@[protected]
noncomputable def smooth_bump_covering.fintype {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s)  :

The index type of a smooth_bump_covering of a compact manifold is finite.

Equations
noncomputable def smooth_bump_covering.to_bump_covering {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] :
s

Reinterpret a smooth_bump_covering as a continuous bump_covering. Note that not every f : bump_covering ι M s with smooth functions f i is a smooth_bump_covering.

Equations
@[simp]
theorem smooth_bump_covering.is_subordinate_to_bump_covering {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} [t2_space M] {f : M s} {U : M → set M} :
f.to_bump_covering.is_subordinate (λ (i : ι), U (f.c i))
theorem smooth_bump_covering.is_subordinate.to_bump_covering {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} [t2_space M] {f : M s} {U : M → set M} :
f.to_bump_covering.is_subordinate (λ (i : ι), U (f.c i))

Alias of the reverse direction of smooth_bump_covering.is_subordinate_to_bump_covering.

noncomputable def smooth_bump_covering.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] :
s

Every smooth_bump_covering defines a smooth partition of unity.

Equations
theorem smooth_bump_covering.to_smooth_partition_of_unity_apply {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] (i : ι) (x : M) :
((fs.to_smooth_partition_of_unity) i) x = (fs i) x * finprod (λ (j : ι), finprod (λ (hj : , 1 - (fs j) x))
theorem smooth_bump_covering.to_smooth_partition_of_unity_eq_mul_prod {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] (i : ι) (x : M) (t : finset ι) (ht : ∀ (j : ι), (fs j) x 0j t) :
((fs.to_smooth_partition_of_unity) i) x = (fs i) x * (finset.filter (λ (j : ι), t).prod (λ (j : ι), 1 - (fs j) x)
theorem smooth_bump_covering.exists_finset_to_smooth_partition_of_unity_eventually_eq {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] (i : ι) (x : M) :
∃ (t : finset ι), ((fs.to_smooth_partition_of_unity) i) =ᶠ[nhds x] (fs i) * (finset.filter (λ (j : ι), t).prod (λ (j : ι), 1 - (fs j))
theorem smooth_bump_covering.to_smooth_partition_of_unity_zero_of_zero {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] {i : ι} {x : M} (h : (fs i) x = 0) :
theorem smooth_bump_covering.support_to_smooth_partition_of_unity_subset {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] (i : ι) :
theorem smooth_bump_covering.is_subordinate.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} [t2_space M] {f : M s} {U : M → set M} (h : f.is_subordinate U) :
theorem smooth_bump_covering.sum_to_smooth_partition_of_unity_eq {ι : Type uι} {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {s : set M} (fs : M s) [t2_space M] (x : M) :
finsum (λ (i : ι), ((fs.to_smooth_partition_of_unity) i) x) = 1 - finprod (λ (i : ι), 1 - (fs i) x)
theorem exists_smooth_zero_one_of_closed {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] [t2_space M] {s t : set M} (hs : is_closed s) (ht : is_closed t) (hd : t) :
∃ (f : ), 0 s 1 t ∀ (x : M), f x 1

Given two disjoint closed sets in a Hausdorff σ-compact finite dimensional manifold, there exists an infinitely smooth function that is equal to 0 on one of them and is equal to one on the other.

noncomputable def smooth_partition_of_unity.single {ι : Type uι} {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] (i : ι) (s : set M) :
s

A smooth_partition_of_unity that consists of a single function, uniformly equal to one, defined as an example for inhabited instance.

Equations
@[protected, instance]
noncomputable def smooth_partition_of_unity.inhabited {ι : Type uι} {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] [inhabited ι] (s : set M) :
Equations
theorem smooth_partition_of_unity.exists_is_subordinate {ι : Type uι} {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] [t2_space M] {s : set M} (hs : is_closed s) (U : ι → set M) (ho : ∀ (i : ι), is_open (U i)) (hU : s ⋃ (i : ι), U i) :
∃ (f : s),

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a bump_covering ι X s that is subordinate to U.

theorem exists_cont_mdiff_forall_mem_convex_of_local {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} (I : H) {M : Type uM} [ M] [t2_space M] {t : M → set F} {n : ℕ∞} (ht : ∀ (x : M), (t x)) (Hloc : ∀ (x : M), ∃ (U : set M) (H_1 : U nhds x) (g : M → F), g U ∀ (y : M), y Ug y t y) :
∃ (g : F n), ∀ (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^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also exists_smooth_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local_const.

theorem exists_smooth_forall_mem_convex_of_local {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} (I : H) {M : Type uM} [ M] [t2_space M] {t : M → set F} (ht : ∀ (x : M), (t x)) (Hloc : ∀ (x : M), ∃ (U : set M) (H_1 : U nhds x) (g : M → F), g U ∀ (y : M), y Ug y t y) :
∃ (g : F ), ∀ (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 smooth on U and g y ∈ t y for all y ∈ U. Then there exists a smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also exists_cont_mdiff_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local_const.

theorem exists_smooth_forall_mem_convex_of_local_const {E : Type uE} [ E] {F : Type uF} [ F] {H : Type uH} (I : H) {M : Type uM} [ M] [t2_space M] {t : M → set F} (ht : ∀ (x : M), (t x)) (Hloc : ∀ (x : M), ∃ (c : F), ∀ᶠ (y : M) in nhds x, c t y) :
∃ (g : F ), ∀ (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 vector c : F such that for all y in a neighborhood of x we have c ∈ t y. Then there exists a smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also exists_cont_mdiff_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local.

theorem emetric.exists_smooth_forall_closed_ball_subset {ι : Type uι} {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type u_1} [ M] {K U : ι → set M} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : ), (∀ (x : M), 0 < δ x) ∀ (i : ι) (x : M), x K i (ennreal.of_real (δ x)) U i

Let M be a smooth σ-compact manifold with extended distance. 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 emetric.closed_ball x (δ x) ⊆ U i.

theorem metric.exists_smooth_forall_closed_ball_subset {ι : Type uι} {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type u_1} [metric_space M] [ M] {K U : ι → set M} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : ), (∀ (x : M), 0 < δ x) ∀ (i : ι) (x : M), x K i (δ 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.closed_ball x (δ x) ⊆ U i.