feat(Topology/Support): add tsupport_smul_{left,right} (#9778)

- rename `Function.support_smul_subset_right` to `Function.support_const_smul_subset`

From sphere-eversion; I'm just upstreaming it.

Co-authored-by: grunweg <[email protected]>

Archive/Hairer.lean

@@ -40,7 +40,7 @@ def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
   zero_mem' :=
     ⟨(tsupport_eq_empty_iff.mpr rfl).subset.trans (empty_subset _), contDiff_const (c := 0)⟩
   smul_mem' r f hf :=
-    ⟨(closure_mono <| support_smul_subset_right r f).trans hf.1, contDiff_const.smul hf.2⟩
+    ⟨(closure_mono <| support_const_smul_subset r f).trans hf.1, contDiff_const.smul hf.2⟩
 
 namespace SmoothSupportedOn
 

Mathlib/Algebra/Module/Basic.lean

@@ -765,9 +765,16 @@ theorem Int.smul_one_eq_coe {R : Type*} [Ring R] (m : ℤ) : m • (1 : R) = ↑
 namespace Function
 
 lemma support_smul_subset_left [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :
-    support (f • g) ⊆ support f := fun x hfg hf ↦ hfg <| by rw [Pi.smul_apply', hf, zero_smul]
+    support (f • g) ⊆ support f := fun x hfg hf ↦
+  hfg <| by rw [Pi.smul_apply', hf, zero_smul]
 #align function.support_smul_subset_left Function.support_smul_subset_left
 
+-- Changed (2024-01-21): this lemma was generalised;
+-- the old version is now called `support_const_smul_subset`.
+lemma support_smul_subset_right [Zero M] [SMulZeroClass R M] (f : α → R) (g : α → M) :
+    support (f • g) ⊆ support g :=
+  fun x hbf hf ↦ hbf <| by rw [Pi.smul_apply', hf, smul_zero]
+
 lemma support_const_smul_of_ne_zero [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M]
     (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g :=
   ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne.def, smul_eq_zero, false_or_iff]
@@ -778,10 +785,9 @@ lemma support_smul [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M]
   ext fun _ => smul_ne_zero_iff
 #align function.support_smul Function.support_smul
 
-lemma support_smul_subset_right [Zero M] [SMulZeroClass R M] (a : R) (f : α → M) :
-    support (a • f) ⊆ support f := fun x hbf hf =>
-  hbf <| by rw [Pi.smul_apply, hf, smul_zero]
-#align function.support_smul_subset_right Function.support_smul_subset_right
+lemma support_const_smul_subset [Zero M] [SMulZeroClass R M] (a : R) (f : α → M) :
+    support (a • f) ⊆ support f := support_smul_subset_right (fun _ ↦ a) f
+#align function.support_smul_subset_right Function.support_const_smul_subset
 
 end Function
 

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -1111,7 +1111,7 @@ protected theorem const_smul {𝕜} [TopologicalSpace 𝕜] [AddMonoid β] [Mono
     FinStronglyMeasurable (c • f) μ := by
   refine' ⟨fun n => c • hf.approx n, fun n => _, fun x => (hf.tendsto_approx x).const_smul c⟩
   rw [SimpleFunc.coe_smul]
-  refine' (measure_mono (support_smul_subset_right c _)).trans_lt (hf.fin_support_approx n)
+  exact (measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)
 #align measure_theory.fin_strongly_measurable.const_smul MeasureTheory.FinStronglyMeasurable.const_smul
 
 end Arithmetic

Mathlib/RingTheory/HahnSeries.lean

@@ -490,7 +490,7 @@ variable [PartialOrder Γ] {V : Type*} [Monoid R] [AddMonoid V] [DistribMulActio
 instance : SMul R (HahnSeries Γ V) :=
   ⟨fun r x =>
     { coeff := r • x.coeff
-      isPWO_support' := x.isPWO_support.mono (Function.support_smul_subset_right r x.coeff) }⟩
+      isPWO_support' := x.isPWO_support.mono (Function.support_const_smul_subset r x.coeff) }⟩
 
 @[simp]
 theorem smul_coeff {r : R} {x : HahnSeries Γ V} {a : Γ} : (r • x).coeff a = r • x.coeff a :=

Mathlib/Topology/Support.lean

@@ -103,6 +103,10 @@ theorem tsupport_smul_subset_left {M α} [TopologicalSpace X] [Zero M] [Zero α]
   closure_mono <| support_smul_subset_left f g
 #align tsupport_smul_subset_left tsupport_smul_subset_left
 
+theorem tsupport_smul_subset_right {M α} [TopologicalSpace X] [Zero α] [SMulZeroClass M α]
+    (f : X → M) (g : X → α) : (tsupport fun x => f x • g x) ⊆ tsupport g :=
+  closure_mono <| support_smul_subset_right f g
+
 @[to_additive]
 theorem mulTSupport_mul [TopologicalSpace X] [Monoid α] {f g : X → α} :
     (mulTSupport fun x ↦ f x * g x) ⊆ mulTSupport f ∪ mulTSupport g :=