feat: more API on tsupport and operations on functions (#31549)

Variants of [Function.mulSupport_one](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Notation/Support.html#Function.mulSupport_one), [Function.mulSupport_binop_subset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Notation/Support.html#Function.mulSupport_binop_subset), [Function.mulSupport_inv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Support.html#Function.mulSupport_inv), [Function.mulSupport_div](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Support.html#Function.mulSupport_div)... for the topological support.

Author: ADedecker

Archive/Hairer.lean

@@ -38,7 +38,7 @@ variable (𝕜 E F) in
 /-- The set of `C^n` functions supported in a set `s`, as a submodule of the space of functions. -/
 def ContDiffSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
   carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
-  add_mem' hf hg := ⟨tsupport_add.trans <| union_subset hf.1 hg.1, hf.2.add hg.2⟩
+  add_mem' hf hg := ⟨(tsupport_add _ _).trans <| union_subset hf.1 hg.1, hf.2.add hg.2⟩
   zero_mem' :=
     ⟨(tsupport_eq_empty_iff.mpr rfl).subset.trans (empty_subset _), contDiff_const (c := 0)⟩
   smul_mem' r f hf :=

Mathlib/Topology/Algebra/Support.lean

@@ -56,6 +56,20 @@ theorem isClosed_mulTSupport (f : X → α) : IsClosed (mulTSupport f) :=
 theorem mulTSupport_eq_empty_iff {f : X → α} : mulTSupport f = ∅ ↔ f = 1 := by
   rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]
 
+@[to_additive (attr := simp)]
+theorem mulTSupport_fun_one : mulTSupport (fun _ ↦ 1 : X → α) = ∅ := by
+  rw [mulTSupport, mulSupport_fun_one, closure_empty]
+
+@[to_additive (attr := simp)]
+theorem mulTSupport_one : mulTSupport (1 : X → α) = ∅ := by
+  rw [mulTSupport, mulSupport_one, closure_empty]
+
+@[to_additive]
+theorem mulTSupport_binop_subset [One β] [One γ] (op : α → β → γ)
+    (op1 : op 1 1 = 1) (f : X → α) (g : X → β) :
+    mulTSupport (fun x ↦ op (f x) (g x)) ⊆ mulTSupport f ∪ mulTSupport g :=
+  closure_mono (mulSupport_binop_subset op op1 f g) |>.trans closure_union.subset
+
 @[to_additive]
 theorem image_eq_one_of_notMem_mulTSupport {f : X → α} {x : X} (hx : x ∉ mulTSupport f) : f x = 1 :=
   mulSupport_subset_iff'.mp (subset_mulTSupport f) x hx
@@ -86,20 +100,49 @@ theorem tsupport_mul_subset_right {α : Type*} [MulZeroClass α] {f g : X → α
 
 end One
 
-theorem tsupport_smul_subset_left {M α} [TopologicalSpace X] [Zero M] [Zero α] [SMulWithZero M α]
+section Operations
+
+variable [TopologicalSpace X]
+
+@[to_additive (attr := simp)]
+theorem mulTSupport_mul [MulOneClass α] (f g : X → α) :
+    (mulTSupport fun x ↦ f x * g x) ⊆ mulTSupport f ∪ mulTSupport g :=
+  mulTSupport_binop_subset (· * ·) (by simp) f g
+
+@[to_additive]
+theorem mulTSupport_pow [Monoid α] (f : X → α) (n : ℕ) :
+    (mulTSupport fun x => f x ^ n) ⊆ mulTSupport f :=
+  closure_mono <| mulSupport_pow f n
+
+@[to_additive (attr := simp)]
+theorem mulTSupport_fun_inv [DivisionMonoid α] (f : X → α) :
+    (mulTSupport fun x => (f x)⁻¹) = mulTSupport f :=
+  congrArg closure <| mulSupport_fun_inv f
+
+@[to_additive (attr := simp)]
+theorem mulTSupport_inv [DivisionMonoid α] (f : X → α) :
+    mulTSupport f⁻¹ = mulTSupport f :=
+  mulTSupport_fun_inv f
+
+@[to_additive]
+theorem mulTSupport_mul_inv [DivisionMonoid α] (f g : X → α) :
+    (mulTSupport fun x => f x * (g x)⁻¹) ⊆ mulTSupport f ∪ mulTSupport g :=
+  mulTSupport_binop_subset (· * ·⁻¹) (by simp) f g
+
+@[to_additive]
+theorem mulTSupport_div [DivisionMonoid α] (f g : X → α) :
+    (mulTSupport fun x => f x / g x) ⊆ mulTSupport f ∪ mulTSupport g :=
+  mulTSupport_binop_subset (· / ·) one_div_one f g
+
+theorem tsupport_smul_subset_left {M α} [Zero M] [Zero α] [SMulWithZero M α]
     (f : X → M) (g : X → α) : (tsupport fun x => f x • g x) ⊆ tsupport f :=
   closure_mono <| support_smul_subset_left f g
 
-theorem tsupport_smul_subset_right {M α} [TopologicalSpace X] [Zero α] [SMulZeroClass M α]
+theorem tsupport_smul_subset_right {M α} [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] [MulOneClass α] {f g : X → α} :
-    (mulTSupport fun x ↦ f x * g x) ⊆ mulTSupport f ∪ mulTSupport g :=
-  closure_minimal
-    ((mulSupport_mul f g).trans (union_subset_union (subset_mulTSupport _) (subset_mulTSupport _)))
-    (isClosed_closure.union isClosed_closure)
+end Operations
 
 section