feat(topology/support): define topological support and compactly supp…

…orted functions (#11923)

* Also add some variants of the extreme value theorem.

src/algebra/group/to_additive.lean

@@ -204,6 +204,7 @@ meta def tr : bool → list string → list string
 | is_comm ("lt" :: "one" :: s)        := add_comm_prefix is_comm "neg"       :: tr ff s
 | is_comm ("mul" :: "single" :: s)    := add_comm_prefix is_comm "single"    :: tr ff s
 | is_comm ("mul" :: "support" :: s)   := add_comm_prefix is_comm "support"   :: tr ff s
+| is_comm ("mul" :: "tsupport" :: s)  := add_comm_prefix is_comm "tsupport"  :: tr ff s
 | is_comm ("mul" :: "indicator" :: s) := add_comm_prefix is_comm "indicator" :: tr ff s
 | is_comm ("mul" :: s)                := add_comm_prefix is_comm "add"       :: tr ff s
 | is_comm ("smul" :: s)               := add_comm_prefix is_comm "vadd"      :: tr ff s

src/analysis/calculus/specific_functions.lean

@@ -399,11 +399,11 @@ lemma support_eq : support (f : E → ℝ) = euclidean.ball c f.R :=
 by rw [euclidean.ball_eq_preimage, ← f.to_times_cont_diff_bump_of_inner.support_eq,
   ← support_comp_eq_preimage, coe_eq_comp]
 
-lemma closure_support_eq : closure (support f) = euclidean.closed_ball c f.R :=
-by rw [f.support_eq, euclidean.closure_ball _ f.R_pos]
+lemma tsupport_eq : tsupport f = euclidean.closed_ball c f.R :=
+by rw [tsupport, f.support_eq, euclidean.closure_ball _ f.R_pos]
 
-lemma compact_closure_support : is_compact (closure (support f)) :=
-by { rw f.closure_support_eq, exact euclidean.is_compact_closed_ball }
+protected lemma has_compact_support : has_compact_support f :=
+by simp_rw [has_compact_support, f.tsupport_eq, euclidean.is_compact_closed_ball]
 
 lemma eventually_eq_one_of_mem_ball (h : x ∈ euclidean.ball c f.r) :
   f =ᶠ[𝓝 x] 1 :=
@@ -424,10 +424,10 @@ protected lemma times_cont_diff_within_at {s n} :
   times_cont_diff_within_at ℝ n f s x :=
 f.times_cont_diff_at.times_cont_diff_within_at
 
-lemma exists_closure_support_subset {s : set E} (hs : s ∈ 𝓝 c) :
-  ∃ f : times_cont_diff_bump c, closure (support f) ⊆ s :=
+lemma exists_tsupport_subset {s : set E} (hs : s ∈ 𝓝 c) :
+  ∃ f : times_cont_diff_bump c, tsupport f ⊆ s :=
 let ⟨R, h0, hR⟩ := euclidean.nhds_basis_closed_ball.mem_iff.1 hs
-in ⟨⟨⟨R / 2, R, half_pos h0, half_lt_self h0⟩⟩, by rwa closure_support_eq⟩
+in ⟨⟨⟨R / 2, R, half_pos h0, half_lt_self h0⟩⟩, by rwa tsupport_eq⟩
 
 lemma exists_closure_subset {R : ℝ} (hR : 0 < R)
   {s : set E} (hs : is_closed s) (hsR : s ⊆ euclidean.ball c R) :
@@ -446,15 +446,15 @@ neighborhood `s` there exists an infinitely smooth function with the following p
 
 * `f y = 1` in a neighborhood of `x`;
 * `f y = 0` outside of `s`;
-*  moreover, `closure (support f) ⊆ s` and `closure (support f)` is a compact set;
+*  moreover, `tsupport f ⊆ s` and `f` has compact support;
 * `f y ∈ [0, 1]` for all `y`.
 
 This lemma is a simple wrapper around lemmas about bundled smooth bump functions, see
 `times_cont_diff_bump`. -/
 lemma exists_times_cont_diff_bump_function_of_mem_nhds [normed_group E] [normed_space ℝ E]
   [finite_dimensional ℝ E] {x : E} {s : set E} (hs : s ∈ 𝓝 x) :
   ∃ f : E → ℝ, f =ᶠ[𝓝 x] 1 ∧ (∀ y, f y ∈ Icc (0 : ℝ) 1) ∧ times_cont_diff ℝ ⊤ f ∧
-    is_compact (closure $ support f) ∧ closure (support f) ⊆ s :=
-let ⟨f, hf⟩ := times_cont_diff_bump.exists_closure_support_subset hs in
+    has_compact_support f ∧ tsupport f ⊆ s :=
+let ⟨f, hf⟩ := times_cont_diff_bump.exists_tsupport_subset hs in
 ⟨f, f.eventually_eq_one, λ y, ⟨f.nonneg, f.le_one⟩, f.times_cont_diff,
-  f.compact_closure_support, hf⟩
+  f.has_compact_support, hf⟩

src/analysis/normed/group/basic.lean

@@ -1019,4 +1019,17 @@ lemma tendsto_norm_sub_self_punctured_nhds (a : E) : tendsto (λ x, ∥x - a∥)
 lemma tendsto_norm_nhds_within_zero : tendsto (norm : E → ℝ) (𝓝[≠] 0) (𝓝[>] 0) :=
 tendsto_norm_zero.inf $ tendsto_principal_principal.2 $ λ x, norm_pos_iff.2
 
+/-! Some relations with `has_compact_support` -/
+
+lemma has_compact_support_norm_iff [topological_space α] {f : α → E} :
+  has_compact_support (λ x, ∥ f x ∥) ↔ has_compact_support f :=
+has_compact_support_comp_left $ λ x, norm_eq_zero
+
+alias has_compact_support_norm_iff ↔ _ has_compact_support.norm
+
+lemma continuous.bounded_above_of_compact_support [topological_space α] {f : α → E}
+  (hf : continuous f) (hsupp : has_compact_support f) : ∃ C, ∀ x, ∥f x∥ ≤ C :=
+by simpa [bdd_above_def] using hf.norm.bdd_above_range_of_has_compact_support hsupp.norm
+
+
 end normed_group

src/geometry/manifold/bump_function.lean

@@ -166,7 +166,7 @@ by { rw [euclidean.dist, dist_self], exact f.r_pos }
 lemma support_mem_nhds : support f ∈ 𝓝 c :=
 f.eventually_eq_one.mono $ λ x hx, by { rw hx, exact one_ne_zero }
 
-lemma closure_support_mem_nhds : closure (support f) ∈ 𝓝 c :=
+lemma tsupport_mem_nhds : tsupport f ∈ 𝓝 c :=
 mem_of_superset f.support_mem_nhds subset_closure
 
 lemma c_mem_support : c ∈ support f := mem_of_mem_nhds f.support_mem_nhds
@@ -237,58 +237,57 @@ lemma closed_symm_image_closed_ball :
   is_closed ((ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)) :=
 f.compact_symm_image_closed_ball.is_closed
 
-lemma closure_support_subset_symm_image_closed_ball :
-  closure (support f) ⊆
-    (ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I) :=
+lemma tsupport_subset_symm_image_closed_ball :
+  tsupport f ⊆ (ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I) :=
 begin
-  rw support_eq_symm_image,
+  rw [tsupport, support_eq_symm_image],
   exact closure_minimal (image_subset _ $ inter_subset_inter_left _ ball_subset_closed_ball)
     f.closed_symm_image_closed_ball
 end
 
-lemma closure_support_subset_ext_chart_at_source :
-  closure (support f) ⊆ (ext_chart_at I c).source :=
-calc closure (support f)
+lemma tsupport_subset_ext_chart_at_source :
+  tsupport f ⊆ (ext_chart_at I c).source :=
+calc tsupport f
     ⊆ (ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I) :
-  f.closure_support_subset_symm_image_closed_ball
+  f.tsupport_subset_symm_image_closed_ball
 ... ⊆ (ext_chart_at I c).symm '' (ext_chart_at I c).target :
   image_subset _ f.closed_ball_subset
 ... = (ext_chart_at I c).source :
   (ext_chart_at I c).symm_image_target_eq_source
 
-lemma closure_support_subset_chart_at_source :
-  closure (support f) ⊆ (chart_at H c).source :=
-by simpa only [ext_chart_at_source] using f.closure_support_subset_ext_chart_at_source
+lemma tsupport_subset_chart_at_source :
+  tsupport f ⊆ (chart_at H c).source :=
+by simpa only [ext_chart_at_source] using f.tsupport_subset_ext_chart_at_source
 
-lemma compact_closure_support : is_compact (closure $ support f) :=
+protected lemma has_compact_support : has_compact_support f :=
 compact_of_is_closed_subset f.compact_symm_image_closed_ball is_closed_closure
- f.closure_support_subset_symm_image_closed_ball
+ f.tsupport_subset_symm_image_closed_ball
 
 variables (I c)
 
 /-- The closures of supports of smooth bump functions centered at `c` form a basis of `𝓝 c`.
 In other words, each of these closures is a neighborhood of `c` and each neighborhood of `c`
-includes `closure (support f)` for some `f : smooth_bump_function I c`. -/
-lemma nhds_basis_closure_support :
-  (𝓝 c).has_basis (λ f : smooth_bump_function I c, true) (λ f, closure $ support f) :=
+includes `tsupport f` for some `f : smooth_bump_function I c`. -/
+lemma nhds_basis_tsupport :
+  (𝓝 c).has_basis (λ f : smooth_bump_function I c, true) (λ f, tsupport f) :=
 begin
   have : (𝓝 c).has_basis (λ f : smooth_bump_function I c, true)
     (λ f, (ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)),
   { rw [← ext_chart_at_symm_map_nhds_within_range I c],
     exact nhds_within_range_basis.map _ },
-  refine this.to_has_basis' (λ f hf, ⟨f, trivial, f.closure_support_subset_symm_image_closed_ball⟩)
-    (λ f _, f.closure_support_mem_nhds),
+  refine this.to_has_basis' (λ f hf, ⟨f, trivial, f.tsupport_subset_symm_image_closed_ball⟩)
+    (λ f _, f.tsupport_mem_nhds),
 end
 
 variable {c}
 
 /-- Given `s ∈ 𝓝 c`, the supports of smooth bump functions `f : smooth_bump_function I c` such that
-`closure (support f) ⊆ s` form a basis of `𝓝 c`.  In other words, each of these supports is a
+`tsupport f ⊆ s` form a basis of `𝓝 c`.  In other words, each of these supports is a
 neighborhood of `c` and each neighborhood of `c` includes `support f` for some `f :
-smooth_bump_function I c` such that `closure (support f) ⊆ s`. -/
+smooth_bump_function I c` such that `tsupport f ⊆ s`. -/
 lemma nhds_basis_support {s : set M} (hs : s ∈ 𝓝 c) :
-  (𝓝 c).has_basis (λ f : smooth_bump_function I c, closure (support f) ⊆ s) (λ f, support f) :=
-((nhds_basis_closure_support I c).restrict_subset hs).to_has_basis'
+  (𝓝 c).has_basis (λ f : smooth_bump_function I c, tsupport f ⊆ s) (λ f, support f) :=
+((nhds_basis_tsupport I c).restrict_subset hs).to_has_basis'
   (λ f hf, ⟨f, hf.2, subset_closure⟩) (λ f hf, f.support_mem_nhds)
 
 variables [smooth_manifold_with_corners I M] {I}
@@ -297,7 +296,7 @@ variables [smooth_manifold_with_corners I M] {I}
 protected lemma smooth : smooth I 𝓘(ℝ) f :=
 begin
   refine times_cont_mdiff_of_support (λ x hx, _),
-  have : x ∈ (chart_at H c).source := f.closure_support_subset_chart_at_source hx,
+  have : x ∈ (chart_at H c).source := f.tsupport_subset_chart_at_source hx,
   refine times_cont_mdiff_at.congr_of_eventually_eq _
     (f.eq_on_source.eventually_eq_of_mem $ is_open.mem_nhds (chart_at _ _).open_source this),
   exact f.to_times_cont_diff_bump.times_cont_diff_at.times_cont_mdiff_at.comp _
@@ -316,9 +315,9 @@ lemma smooth_smul {G} [normed_group G] [normed_space ℝ G]
 begin
   apply times_cont_mdiff_of_support (λ x hx, _),
   have : x ∈ (chart_at H c).source,
-  calc x ∈ closure (support (λ x, f x • g x)) : hx
-     ... ⊆ closure (support f) : closure_mono (support_smul_subset_left _ _)
-     ... ⊆ (chart_at _ c).source : f.closure_support_subset_chart_at_source,
+  calc x ∈ tsupport (λ x, f x • g x) : hx
+     ... ⊆ tsupport f : closure_mono (support_smul_subset_left _ _)
+     ... ⊆ (chart_at _ c).source : f.tsupport_subset_chart_at_source,
   exact f.smooth_at.smul ((hg _ this).times_cont_mdiff_at $
     is_open.mem_nhds (chart_at _ _).open_source this)
 end

src/geometry/manifold/partition_of_unity.lean

@@ -32,7 +32,7 @@ functions `f i : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯`, `i : ι`, such that
 * 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 `closure (support (f i)) ⊆ U (f i).c`. This notion is a bit more general than
+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`.
 
@@ -150,7 +150,7 @@ lemma sum_nonneg (x : M) : 0 ≤ ∑ᶠ i, f i x := f.to_partition_of_unity.sum_
 /-- 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, closure (support (f i)) ⊆ U i
+∀ 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} :
@@ -218,12 +218,12 @@ rfl
 
 /--
 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 `closure (support (f i)) ⊆ U (f i).c`. This notion is a bit more general than
+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`.
 -/
 def is_subordinate {s : set M} (f : smooth_bump_covering ι I M s) (U : M → set M) :=
-∀ i, closure (support $ f i) ⊆ U (f.c i)
+∀ i, tsupport (f i) ⊆ U (f.c i)
 
 lemma is_subordinate.support_subset {fs : smooth_bump_covering ι I M s} {U : M → set M}
   (h : fs.is_subordinate U) (i : ι) :
@@ -257,7 +257,7 @@ begin
   { refine (mem_Union.1 $ hsV hx).imp (λ i hi, _),
     exact ((f i).update_r _ _).eventually_eq_one_of_dist_lt
       ((f i).support_subset_source $ hVf _ hi) (hr i hi).2 },
-  { simpa only [coe_mk, smooth_bump_function.support_update_r] using hfU i }
+  { simpa only [coe_mk, smooth_bump_function.support_update_r, tsupport] using hfU i }
 end
 
 variables {I M}

src/geometry/manifold/times_cont_mdiff.lean

@@ -979,11 +979,11 @@ times_cont_mdiff_within_at_one
 end id
 
 lemma times_cont_mdiff_of_support {f : M → F}
-  (hf : ∀ x ∈ closure (support f), times_cont_mdiff_at I 𝓘(𝕜, F) n f x) :
+  (hf : ∀ x ∈ tsupport f, times_cont_mdiff_at I 𝓘(𝕜, F) n f x) :
   times_cont_mdiff I 𝓘(𝕜, F) n f :=
 begin
   intro x,
-  by_cases hx : x ∈ closure (support f),
+  by_cases hx : x ∈ tsupport f,
   { exact hf x hx },
   { refine times_cont_mdiff_at.congr_of_eventually_eq _ (eventually_eq_zero_nhds.2 hx),
     exact times_cont_mdiff_at_const }

src/measure_theory/integral/integrable_on.lean

@@ -421,11 +421,10 @@ lemma continuous.integrable_on_interval_oc [borel_space E]
 hf.integrable_on_Ioc
 
 /-- A continuous function with compact closure of the support is integrable on the whole space. -/
-lemma continuous.integrable_of_compact_closure_support
+lemma continuous.integrable_of_has_compact_support
   [topological_space α] [opens_measurable_space α] [t2_space α] [borel_space E]
   {μ : measure α} [is_locally_finite_measure μ] {f : α → E} (hf : continuous f)
-  (hfc : is_compact (closure $ support f)) :
-  integrable f μ :=
+  (hfc : has_compact_support f) : integrable f μ :=
 begin
   rw [← indicator_eq_self.2 (@subset_closure _ _ (support f)),
     integrable_indicator_iff is_closed_closure.measurable_set],

src/topology/algebra/order/compact.lean

@@ -210,21 +210,33 @@ lemma is_compact.exists_forall_ge :
   ∃x∈s, ∀y∈s, f y ≤ f x :=
 @is_compact.exists_forall_le (order_dual α) _ _ _ _ _
 
+/-- The **extreme value theorem**: if a continuous function `f` is larger than a value in its range
+away from compact sets, then it has a global minimum. -/
+lemma _root_.continuous.exists_forall_le' {f : β → α} (hf : continuous f) (x₀ : β)
+  (h : ∀ᶠ x in cocompact β, f x₀ ≤ f x) : ∃ (x : β), ∀ (y : β), f x ≤ f y :=
+begin
+  obtain ⟨K : set β, hK : is_compact K, hKf : ∀ x ∉ K, f x₀ ≤ f x⟩ :=
+  (has_basis_cocompact.eventually_iff).mp h,
+  obtain ⟨x, -, hx⟩ : ∃ x ∈ insert x₀ K, ∀ y ∈ insert x₀ K, f x ≤ f y :=
+  (hK.insert x₀).exists_forall_le (nonempty_insert _ _) hf.continuous_on,
+  refine ⟨x, λ y, _⟩,
+  by_cases hy : y ∈ K,
+  exacts [hx y (or.inr hy), (hx _ (or.inl rfl)).trans (hKf y hy)]
+end
+
+/-- The **extreme value theorem**: if a continuous function `f` is smaller than a value in its range
+away from compact sets, then it has a global maximum. -/
+lemma _root_.continuous.exists_forall_ge' {f : β → α} (hf : continuous f) (x₀ : β)
+  (h : ∀ᶠ x in cocompact β, f x ≤ f x₀) : ∃ (x : β), ∀ (y : β), f y ≤ f x :=
+@continuous.exists_forall_le' (order_dual α) _ _ _ _ _ _ hf x₀ h
+
 /-- The **extreme value theorem**: if a continuous function `f` tends to infinity away from compact
 sets, then it has a global minimum. -/
-lemma continuous.exists_forall_le [nonempty β] {f : β → α}
+lemma _root_.continuous.exists_forall_le [nonempty β] {f : β → α}
   (hf : continuous f) (hlim : tendsto f (cocompact β) at_top) :
   ∃ x, ∀ y, f x ≤ f y :=
-begin
-  inhabit β,
-  obtain ⟨s : set β, hsc : is_compact s, hsf : ∀ x ∉ s, f default ≤ f x⟩ :=
-    (has_basis_cocompact.tendsto_iff at_top_basis).1 hlim (f default) trivial,
-  obtain ⟨x, -, hx⟩ : ∃ x ∈ insert default s, ∀ y ∈ insert default s, f x ≤ f y :=
-    (hsc.insert default).exists_forall_le (nonempty_insert _ _) hf.continuous_on,
-  refine ⟨x, λ y, _⟩,
-  by_cases hy : y ∈ s,
-  exacts [hx y (or.inr hy), (hx _ (or.inl rfl)).trans (hsf y hy)]
-end
+by { inhabit β, exact hf.exists_forall_le' default (hlim.eventually $ eventually_ge_at_top _) }
+
 
 /-- The **extreme value theorem**: if a continuous function `f` tends to negative infinity away from
 compact sets, then it has a global maximum. -/
@@ -233,6 +245,60 @@ lemma continuous.exists_forall_ge [nonempty β] {f : β → α}
   ∃ x, ∀ y, f y ≤ f x :=
 @continuous.exists_forall_le (order_dual α) _ _ _ _ _ _ _ hf hlim
 
+/-- A continuous function with compact support has a global minimum. -/
+@[to_additive]
+lemma _root_.continuous.exists_forall_le_of_has_compact_mul_support [nonempty β] [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  ∃ (x : β), ∀ (y : β), f x ≤ f y :=
+begin
+  -- Proof sketch: we use `continuous.exists_forall_le'` with as `x₀` any element outside the
+  -- support of `f`, if such an element exists (and otherwise an arbitrary element).
+  refine hf.exists_forall_le' (classical.epsilon $ λ x, f x = 1)
+    (eventually_of_mem h.compl_mem_cocompact $ λ x hx, _),
+  have : f x = 1 := nmem_mul_support.mp (mt (λ h2x, subset_closure h2x) hx),
+  exact ((classical.epsilon_spec ⟨x, this⟩).trans this.symm).le
+end
+
+/-- A continuous function with compact support has a global maximum. -/
+@[to_additive]
+lemma continuous.exists_forall_ge_of_has_compact_mul_support [nonempty β] [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  ∃ (x : β), ∀ (y : β), f y ≤ f x :=
+@continuous.exists_forall_le_of_has_compact_mul_support (order_dual α) _ _ _ _ _ _ _ _ hf h
+
+/-- A continuous function with compact support is bounded below. -/
+@[to_additive]
+lemma continuous.bdd_below_range_of_has_compact_mul_support [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  bdd_below (range f) :=
+begin
+  casesI is_empty_or_nonempty β with hβ hβ,
+  { rw range_eq_empty_iff.mpr, exact bdd_below_empty, exact hβ },
+  obtain ⟨x, hx⟩ := hf.exists_forall_le_of_has_compact_mul_support h,
+  refine ⟨f x, _⟩, rintro _ ⟨x', rfl⟩, exact hx x'
+end
+
+/-- A continuous function with compact support is bounded above. -/
+@[to_additive]
+lemma continuous.bdd_above_range_of_has_compact_mul_support [has_one α]
+  {f : β → α} (hf : continuous f) (h : has_compact_mul_support f) :
+  bdd_above (range f) :=
+@continuous.bdd_below_range_of_has_compact_mul_support (order_dual α) _ _ _ _ _ _ _ hf h
+
+/-- A continuous function is bounded below on a compact set. -/
+lemma is_compact.bdd_below_image {f : β → α} {K : set β}
+  (hK : is_compact K) (hf : continuous_on f K) : bdd_below (f '' K) :=
+begin
+  rcases eq_empty_or_nonempty K with rfl|h, { rw [image_empty], exact bdd_below_empty },
+  obtain ⟨c, -, hc⟩ := hK.exists_forall_le h hf,
+  refine ⟨f c, _⟩, rintro _ ⟨x, hx, rfl⟩, exact hc x hx
+end
+
+/-- A continuous function is bounded above on a compact set. -/
+lemma is_compact.bdd_above_image {f : β → α} {K : set β}
+  (hK : is_compact K) (hf : continuous_on f K) : bdd_above (f '' K) :=
+@is_compact.bdd_below_image (order_dual α) _ _ _ _ _ _ _ hK hf
+
 /-!
 ### Image of a closed interval
 -/

src/topology/homeomorph.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton
 -/
 import topology.dense_embedding
+import topology.support
 import data.equiv.fin
 
 /-!
@@ -230,6 +231,11 @@ by rw [← preimage_symm, preimage_interior]
 lemma preimage_frontier (h : α ≃ₜ β) (s : set β) : h ⁻¹' (frontier s) = frontier (h ⁻¹' s) :=
 h.is_open_map.preimage_frontier_eq_frontier_preimage h.continuous _
 
+@[to_additive]
+lemma _root_.has_compact_mul_support.comp_homeomorph {M} [has_one M] {f : β → M}
+  (hf : has_compact_mul_support f) (φ : α ≃ₜ β) : has_compact_mul_support (f ∘ φ) :=
+hf.comp_closed_embedding φ.closed_embedding
+
 @[simp] lemma map_nhds_eq (h : α ≃ₜ β) (x : α) : map h (𝓝 x) = 𝓝 (h x) :=
 h.embedding.map_nhds_of_mem _ (by simp)