feat(topology/partition_of_unity): local to global (#15490)

Use partitions of unity to construct global maps.

Motivated by discussions with @PatrickMassot . Useful for the sphere eversion project and probably duplicates some lemmas from that project.

src/analysis/convex/combination.lean

@@ -23,7 +23,7 @@ mathematical arguments go: one doesn't change weights, but merely adds some. Thi
 lemmas unconditional on the sum of the weights being `1`.
 -/
 
-open set
+open set function
 open_locale big_operators classical pointwise
 
 universes u u'
@@ -73,7 +73,7 @@ lemma finset.center_mass_segment'
   (s : finset ι) (t : finset ι') (ws : ι → R) (zs : ι → E) (wt : ι' → R) (zt : ι' → E)
   (hws : ∑ i in s, ws i = 1) (hwt : ∑ i in t, wt i = 1) (a b : R) (hab : a + b = 1) :
   a • s.center_mass ws zs + b • t.center_mass wt zt =
-    (s.map function.embedding.inl ∪ t.map function.embedding.inr).center_mass
+    (s.map embedding.inl ∪ t.map embedding.inr).center_mass
       (sum.elim (λ i, a * ws i) (λ j, b * wt j))
       (sum.elim zs zt) :=
 begin
@@ -153,6 +153,26 @@ lemma convex.sum_mem (hs : convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : 
 by simpa only [h₁, center_mass, inv_one, one_smul] using
   hs.center_mass_mem h₀ (h₁.symm ▸ zero_lt_one) hz
 
+/-- A version of `convex.sum_mem` for `finsum`s. If `s` is a convex set, `w : ι → R` is a family of
+nonnegative weights with sum one and `z : ι → E` is a family of elements of a module over `R` such
+that `z i ∈ s` whenever `w i ≠ 0``, then the sum `∑ᶠ i, w i • z i` belongs to `s`. See also
+`partition_of_unity.finsum_smul_mem_convex`. -/
+lemma convex.finsum_mem {ι : Sort*} {w : ι → R} {z : ι → E} {s : set E}
+  (hs : convex R s) (h₀ : ∀ i, 0 ≤ w i) (h₁ : ∑ᶠ i, w i = 1) (hz : ∀ i, w i ≠ 0 → z i ∈ s) :
+  ∑ᶠ i, w i • z i ∈ s :=
+begin
+  have hfin_w : (support (w ∘ plift.down)).finite,
+  { by_contra H,
+    rw [finsum, dif_neg H] at h₁,
+    exact zero_ne_one h₁ },
+  have hsub : support ((λ i, w i • z i) ∘ plift.down) ⊆ hfin_w.to_finset,
+    from (support_smul_subset_left _ _).trans hfin_w.coe_to_finset.ge,
+  rw [finsum_eq_sum_plift_of_support_subset hsub],
+  refine hs.sum_mem (λ _ _, h₀ _) _ (λ i hi, hz _ _),
+  { rwa [finsum, dif_pos hfin_w] at h₁ },
+  { rwa [hfin_w.mem_to_finset] at hi }
+end
+
 lemma convex_iff_sum_mem :
   convex R s ↔
     (∀ (t : finset E) (w : E → R),

src/analysis/convex/partition_of_unity.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import topology.partition_of_unity
+import analysis.convex.combination
+
+/-!
+# Partition of unity and convex sets
+
+In this file we prove the following lemma, see `exists_continuous_forall_mem_convex_of_local`. Let
+`X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be a
+topological real vector space. Let `t : X → set E` be a family of convex sets. Suppose that for each
+point `x : X`, there exists a neighborhood `U ∈ 𝓝 X` and a function `g : X → E` that is continuous
+on `U` and sends each `y ∈ U` to a point of `t y`. Then there exists a continuous map `g : C(X, E)`
+such that `g x ∈ t x` for all `x`.
+
+We also formulate a useful corollary, see `exists_continuous_forall_mem_convex_of_local_const`, that
+assumes that local functions `g` are constants.
+
+## Tags
+
+partition of unity
+-/
+
+open set function
+open_locale big_operators topological_space
+
+variables {ι X E : Type*} [topological_space X] [add_comm_group E] [module ℝ E]
+
+lemma partition_of_unity.finsum_smul_mem_convex {s : set X} (f : partition_of_unity ι X s)
+  {g : ι → X → E} {t : set E} {x : X} (hx : x ∈ s) (hg : ∀ i, f i x ≠ 0 → g i x ∈ t)
+  (ht : convex ℝ t) :
+  ∑ᶠ i, f i x • g i x ∈ t :=
+ht.finsum_mem (λ i, f.nonneg _ _) (f.sum_eq_one hx) hg
+
+variables [normal_space X] [paracompact_space X] [topological_space E] [has_continuous_add E]
+  [has_continuous_smul ℝ E] {t : X → set E}
+
+/-- Let `X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be
+a topological real vector space. Let `t : X → set E` be a family of convex sets. Suppose that for
+each point `x : X`, there exists a neighborhood `U ∈ 𝓝 X` and a function `g : X → E` that is
+continuous on `U` and sends each `y ∈ U` to a point of `t y`. Then there exists a continuous map
+`g : C(X, E)` such that `g x ∈ t x` for all `x`. See also
+`exists_continuous_forall_mem_convex_of_local_const`. -/
+lemma exists_continuous_forall_mem_convex_of_local (ht : ∀ x, convex ℝ (t x))
+  (H : ∀ x : X, ∃ (U ∈ 𝓝 x) (g : X → E), continuous_on g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃
+  g : C(X, E), ∀ x, g x ∈ t x :=
+begin
+  choose U hU g hgc hgt using H,
+  obtain ⟨f, hf⟩ := partition_of_unity.exists_is_subordinate is_closed_univ (λ x, interior (U x))
+    (λ x, is_open_interior) (λ x hx, mem_Union.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩),
+  refine ⟨⟨λ x, ∑ᶠ i, f i x • g i x,
+    hf.continuous_finsum_smul (λ i, is_open_interior) $ λ i, (hgc i).mono interior_subset⟩,
+    λ x, f.finsum_smul_mem_convex (mem_univ x) (λ i hi, hgt _ _ _) (ht _)⟩,
+  exact interior_subset (hf _ $ subset_closure hi)
+end
+
+/-- Let `X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be
+a topological real vector space. Let `t : X → set E` be a family of convex sets. Suppose that for
+each point `x : X`, there exists a vector `c : E` that belongs to `t y` for all `y` in a
+neighborhood of `x`. Then there exists a continuous map `g : C(X, E)` such that `g x ∈ t x` for all
+`x`. See also `exists_continuous_forall_mem_convex_of_local`. -/
+lemma exists_continuous_forall_mem_convex_of_local_const (ht : ∀ x, convex ℝ (t x))
+  (H : ∀ x : X, ∃ c : E, ∀ᶠ y in 𝓝 x, c ∈ t y) :
+  ∃ g : C(X, E), ∀ x, g x ∈ t x :=
+exists_continuous_forall_mem_convex_of_local ht $ λ x,
+  let ⟨c, hc⟩ := H x in ⟨_, hc, λ _, c, continuous_on_const, λ y, id⟩

src/geometry/manifold/partition_of_unity.lean

@@ -39,23 +39,24 @@ 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.
-
-## Implementation notes
-
+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.
+  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
 -/
 
-universes uι uE uH uM
+universes uι uE uH uM uF
 
 open function filter finite_dimensional set
 open_locale topological_space manifold classical filter big_operators
@@ -64,6 +65,7 @@ noncomputable theory
 
 variables {ι : Type uι}
 {E : Type uE} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E]
+{F : Type uF} [normed_group F] [normed_space ℝ F]
 {H : Type uH} [topological_space H] (I : model_with_corners ℝ E H)
 {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
 
@@ -121,7 +123,7 @@ variables {ι I M}
 
 namespace smooth_partition_of_unity
 
-variables {s : set M} (f : smooth_partition_of_unity ι I M s)
+variables {s : set M} (f : smooth_partition_of_unity ι I M s) {n : with_top ℕ}
 
 instance {s : set M} : has_coe_to_fun (smooth_partition_of_unity ι I M s)
   (λ _, ι → C^∞⟮I, M; 𝓘(ℝ), ℝ⟯) :=
@@ -147,18 +149,66 @@ lemma le_one (i : ι) (x : M) : f i x ≤ 1 := f.to_partition_of_unity.le_one i
 
 lemma sum_nonneg (x : M) : 0 ≤ ∑ᶠ i, f i x := f.to_partition_of_unity.sum_nonneg x
 
+lemma cont_mdiff_smul {g : M → F} {i} (hg : ∀ x ∈ tsupport (f i), cont_mdiff_at I 𝓘(ℝ, F) n g x) :
+  cont_mdiff I 𝓘(ℝ, F) n (λ x, f i x • g x) :=
+cont_mdiff_of_support $ λ x hx, ((f i).cont_mdiff.cont_mdiff_at.of_le le_top).smul $ hg x $
+  tsupport_smul_subset_left _ _ hx
+
+lemma smooth_smul {g : M → F} {i} (hg : ∀ x ∈ tsupport (f i), smooth_at I 𝓘(ℝ, F) g x) :
+  smooth I 𝓘(ℝ, F) (λ x, f i x • g x) :=
+f.cont_mdiff_smul hg
+
+/-- 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. -/
+lemma cont_mdiff_finsum_smul {g : ι → M → F}
+  (hg : ∀ i (x ∈ tsupport (f i)), cont_mdiff_at I 𝓘(ℝ, F) n (g i) x) :
+  cont_mdiff I 𝓘(ℝ, F) n (λ x, ∑ᶠ i, f i x • g i x) :=
+cont_mdiff_finsum (λ i, f.cont_mdiff_smul (hg i)) $ f.locally_finite.subset $
+  λ i, support_smul_subset_left _ _
+
+/-- 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. -/
+lemma smooth_finsum_smul {g : ι → M → F}
+  (hg : ∀ i (x ∈ tsupport (f i)), smooth_at I 𝓘(ℝ, F) (g i) x) :
+  smooth I 𝓘(ℝ, F) (λ x, ∑ᶠ i, f i x • g i x) :=
+f.cont_mdiff_finsum_smul hg
+
+lemma finsum_smul_mem_convex {g : ι → M → F} {t : set F} {x : M} (hx : x ∈ s)
+  (hg : ∀ i, f i x ≠ 0 → g i x ∈ t) (ht : convex ℝ t) :
+  ∑ᶠ i, f i x • g i x ∈ t :=
+ht.finsum_mem (λ i, f.nonneg _ _) (f.sum_eq_one hx) hg
+
 /-- 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`. -/
 def is_subordinate (f : smooth_partition_of_unity ι I M s) (U : ι → set M) :=
 ∀ i, tsupport (f i) ⊆ U i
 
-@[simp] lemma is_subordinate_to_partition_of_unity {f : smooth_partition_of_unity ι I M s}
-  {U : ι → set M} :
+variables {f} {U : ι → set M}
+
+@[simp] lemma is_subordinate_to_partition_of_unity :
   f.to_partition_of_unity.is_subordinate U ↔ f.is_subordinate U :=
 iff.rfl
 
 alias is_subordinate_to_partition_of_unity ↔ _ is_subordinate.to_partition_of_unity
 
+/-- 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. -/
+lemma is_subordinate.cont_mdiff_finsum_smul {g : ι → M → F} (hf : f.is_subordinate U)
+  (ho : ∀ i, is_open (U i)) (hg : ∀ i, cont_mdiff_on I 𝓘(ℝ, F) n (g i) (U i)) :
+  cont_mdiff I 𝓘(ℝ, F) n (λ x, ∑ᶠ i, f i x • g i x) :=
+f.cont_mdiff_finsum_smul $ λ i x hx, (hg i).cont_mdiff_at $ (ho i).mem_nhds (hf i hx)
+
+/-- 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. -/
+lemma is_subordinate.smooth_finsum_smul {g : ι → M → F} (hf : f.is_subordinate U)
+  (ho : ∀ i, is_open (U i)) (hg : ∀ i, smooth_on I 𝓘(ℝ, F) (g i) (U i)) :
+  smooth I 𝓘(ℝ, F) (λ x, ∑ᶠ i, f i x • g i x) :=
+hf.cont_mdiff_finsum_smul ho hg
+
 end smooth_partition_of_unity
 
 namespace bump_covering
@@ -372,8 +422,6 @@ begin
   exact nmem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)
 end
 
-variable {I}
-
 namespace smooth_partition_of_unity
 
 /-- A `smooth_partition_of_unity` that consists of a single function, uniformly equal to one,
@@ -388,7 +436,7 @@ def single (i : ι) (s : set M) : smooth_partition_of_unity ι I M s :=
   end
 
 instance [inhabited ι] (s : set M) : inhabited (smooth_partition_of_unity ι I M s) :=
-⟨single default s⟩
+⟨single I default s⟩
 
 variables [t2_space M] [sigma_compact_space M]
 
@@ -410,3 +458,47 @@ begin
 end
 
 end smooth_partition_of_unity
+
+variables [sigma_compact_space M] [t2_space M] {t : M → set F} {n : with_top ℕ}
+
+/-- 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`. -/
+lemma exists_cont_mdiff_forall_mem_convex_of_local (ht : ∀ x, convex ℝ (t x))
+  (Hloc : ∀ x : M, ∃ (U ∈ 𝓝 x) (g : M → F), cont_mdiff_on I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) :
+  ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
+begin
+  choose U hU g hgs hgt using Hloc,
+  obtain ⟨f, hf⟩ := smooth_partition_of_unity.exists_is_subordinate I is_closed_univ
+    (λ x, interior (U x)) (λ x, is_open_interior)
+    (λ x hx, mem_Union.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩),
+  refine ⟨⟨λ x, ∑ᶠ i, f i x • g i x,
+    hf.cont_mdiff_finsum_smul (λ i, is_open_interior) $ λ i, (hgs i).mono interior_subset⟩,
+    λ x, f.finsum_smul_mem_convex (mem_univ x) (λ i hi, hgt _ _ _) (ht _)⟩,
+  exact interior_subset (hf _ $ subset_closure hi)
+end
+
+/-- 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`. -/
+lemma exists_smooth_forall_mem_convex_of_local (ht : ∀ x, convex ℝ (t x))
+  (Hloc : ∀ x : M, ∃ (U ∈ 𝓝 x) (g : M → F), smooth_on I 𝓘(ℝ, F) g U ∧ ∀ y ∈ U, g y ∈ t y) :
+  ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
+exists_cont_mdiff_forall_mem_convex_of_local I ht Hloc
+
+/-- 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`. -/
+lemma exists_smooth_forall_mem_convex_of_local_const (ht : ∀ x, convex ℝ (t x))
+  (Hloc : ∀ x : M, ∃ c : F, ∀ᶠ y in 𝓝 x, c ∈ t y) :
+  ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
+exists_smooth_forall_mem_convex_of_local I ht $ λ x,
+  let ⟨c, hc⟩ := Hloc x in ⟨_, hc, λ _, c, smooth_on_const, λ y, id⟩

src/topology/partition_of_unity.lean

@@ -125,24 +125,51 @@ variables {ι : Type u} {X : Type v} [topological_space X]
 
 namespace partition_of_unity
 
-variables {s : set X} (f : partition_of_unity ι X s)
+variables {E : Type*} [add_comm_monoid E] [smul_with_zero ℝ E] [topological_space E]
+  [has_continuous_smul ℝ E] {s : set X} (f : partition_of_unity ι X s)
 
 instance : has_coe_to_fun (partition_of_unity ι X s) (λ _, ι → C(X, ℝ)) := ⟨to_fun⟩
 
-protected lemma locally_finite : locally_finite (λ i, support (f i)) :=
-f.locally_finite'
+protected lemma locally_finite : locally_finite (λ i, support (f i)) := f.locally_finite'
+
+lemma locally_finite_tsupport : locally_finite (λ i, tsupport (f i)) := f.locally_finite.closure
 
 lemma nonneg (i : ι) (x : X) : 0 ≤ f i x := f.nonneg' i x
 
 lemma sum_eq_one {x : X} (hx : x ∈ s) : ∑ᶠ i, f i x = 1 := f.sum_eq_one' x hx
 
+/-- If `f` is a partition of unity on `s`, then for every `x ∈ s` there exists an index `i` such
+that `0 < f i x`. -/
+lemma exists_pos {x : X} (hx : x ∈ s) : ∃ i, 0 < f i x :=
+begin
+  have H := f.sum_eq_one hx,
+  contrapose! H,
+  simpa only [λ i, (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one
+end
+
 lemma sum_le_one (x : X) : ∑ᶠ i, f i x ≤ 1 := f.sum_le_one' x
 
 lemma sum_nonneg (x : X) : 0 ≤ ∑ᶠ i, f i x := finsum_nonneg $ λ i, f.nonneg i x
 
 lemma le_one (i : ι) (x : X) : f i x ≤ 1 :=
 (single_le_finsum i (f.locally_finite.point_finite x) (λ j, f.nonneg j x)).trans (f.sum_le_one x)
 
+/-- If `f` is a partition of unity on `s : set X` and `g : X → E` is continuous at every point of
+the topological support of some `f i`, then `λ x, f i x • g x` is continuous on the whole space. -/
+lemma continuous_smul {g : X → E} {i : ι} (hg : ∀ x ∈ tsupport (f i), continuous_at g x) :
+  continuous (λ x, f i x • g x) :=
+continuous_of_tsupport $ λ x hx, ((f i).continuous_at x).smul $
+  hg x $ tsupport_smul_subset_left _ _ hx
+
+/-- If `f` is a partition of unity on a set `s : set X` and `g : ι → X → E` is a family of functions
+such that each `g i` is continuous at every point of the topological support of `f i`, then the sum
+`λ x, ∑ᶠ i, f i x • g i x` is continuous on the whole space. -/
+lemma continuous_finsum_smul [has_continuous_add E] {g : ι → X → E}
+  (hg : ∀ i (x ∈ tsupport (f i)), continuous_at (g i) x) :
+  continuous (λ x, ∑ᶠ i, f i x • g i x) :=
+continuous_finsum (λ i, f.continuous_smul (hg i)) $
+  f.locally_finite.subset $ λ i, support_smul_subset_left _ _
+
 /-- A 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`. -/
 def is_subordinate (U : ι → set X) : Prop :=
@@ -156,6 +183,15 @@ lemma exists_finset_nhd_support_subset {U : ι → set X}
     support (λ i, f i z) ⊆ is :=
 f.locally_finite.exists_finset_nhd_support_subset hso ho x
 
+/-- If `f` is a partition of unity that is subordinate to a family of open sets `U i` and
+`g : ι → X → E` is a family of functions such that each `g i` is continuous on `U i`, then the sum
+`λ x, ∑ᶠ i, f i x • g i x` is a continuous function. -/
+lemma is_subordinate.continuous_finsum_smul [has_continuous_add E] {U : ι → set X}
+  (ho : ∀ i, is_open (U i)) (hf : f.is_subordinate U) {g : ι → X → E}
+  (hg : ∀ i, continuous_on (g i) (U i)) :
+  continuous (λ x, ∑ᶠ i, f i x • g i x) :=
+f.continuous_finsum_smul $ λ i x hx, (hg i).continuous_at $ (ho i).mem_nhds $ hf i hx
+
 end partition_of_unity
 
 namespace bump_covering
@@ -164,11 +200,11 @@ variables {s : set X} (f : bump_covering ι X s)
 
 instance : has_coe_to_fun (bump_covering ι X s) (λ _, ι → C(X, ℝ)) := ⟨to_fun⟩
 
-protected lemma locally_finite : locally_finite (λ i, support (f i)) :=
-f.locally_finite'
+protected lemma locally_finite : locally_finite (λ i, support (f i)) := f.locally_finite'
+
+lemma locally_finite_tsupport : locally_finite (λ i, tsupport (f i)) := f.locally_finite.closure
 
-protected lemma point_finite (x : X) : {i | f i x ≠ 0}.finite :=
-f.locally_finite.point_finite x
+protected lemma point_finite (x : X) : {i | f i x ≠ 0}.finite := f.locally_finite.point_finite x
 
 lemma nonneg (i : ι) (x : X) : 0 ≤ f i x := f.nonneg' i x