feat: make topologicalClosure a ClosureOperator

Author: lua-vr

Mathlib/Analysis/Convex/Cone/InnerDual.lean

@@ -117,12 +117,12 @@ theorem relative_hyperplane_separation {C : ProperCone ℝ E} {f : E →L[ℝ] F
   mp := by
     -- suppose `b ∈ C.map f`
     simp only [map, ClosedSubmodule.map, Submodule.closure, Submodule.topologicalClosure,
-      AddSubmonoid.topologicalClosure, Submodule.coe_toAddSubmonoid, Submodule.map_coe,
-      ContinuousLinearMap.coe_coe,
-      ContinuousLinearMap.coe_restrictScalars', ClosedSubmodule.coe_toSubmodule,
-      ClosedSubmodule.mem_mk, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk,
-      mem_closure_iff_seq_limit, mem_image, SetLike.mem_coe, Classical.skolem, forall_and,
-      mem_innerDual, ContinuousLinearMap.adjoint_inner_right, forall_exists_index, and_imp]
+      AddSubmonoid.topologicalClosure, ClosureOperator.mk₂_apply, Submodule.coe_toAddSubmonoid,
+      ContinuousLinearMap.coe_restrictScalars, Submodule.map_coe, coe_restrictScalars,
+      ContinuousLinearMap.coe_coe, ClosedSubmodule.coe_toSubmodule, ClosedSubmodule.mem_mk,
+      Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, mem_closure_iff_seq_limit,
+      mem_image, SetLike.mem_coe, Classical.skolem, forall_and, mem_innerDual,
+      ContinuousLinearMap.adjoint_inner_right, forall_exists_index, and_imp]
           -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
     rintro x seq hmem hx htends y hinner
     obtain rfl : f ∘ seq = x := funext hx

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -154,9 +154,10 @@ variable [ContinuousAdd M]
 
 /-- The (topological-space) closure of a submodule of a topological `R`-module `M` is itself
 a submodule. -/
-def Submodule.topologicalClosure (s : Submodule R M) : Submodule R M :=
-  { s.toAddSubmonoid.topologicalClosure with
-    smul_mem' := s.mapsTo_smul_closure }
+def Submodule.topologicalClosure : ClosureOperator (Submodule R M) := .mk₂
+  (fun s ↦ { s.toAddSubmonoid.topologicalClosure with smul_mem' := s.mapsTo_smul_closure })
+  (fun _ ↦ subset_closure)
+  (fun _ _ h ↦ closure_minimal h isClosed_closure)
 
 @[simp, norm_cast]
 theorem Submodule.topologicalClosure_coe (s : Submodule R M) :

Mathlib/Topology/Algebra/Monoid.lean

@@ -13,6 +13,7 @@ public import Mathlib.Order.Filter.Pointwise
 public import Mathlib.Topology.Algebra.MulAction
 public import Mathlib.Topology.ContinuousMap.Basic
 public import Mathlib.Topology.Algebra.Monoid.Defs
+public import Mathlib.Order.Closure
 
 /-!
 # Theory of topological monoids
@@ -691,10 +692,12 @@ theorem Submonoid.top_closure_mul_self_eq (s : Submonoid M) :
 itself a submonoid. -/
 @[to_additive /-- The (topological-space) closure of an additive submonoid of a space `M` with
 `ContinuousAdd` is itself an additive submonoid. -/]
-def Submonoid.topologicalClosure (s : Submonoid M) : Submonoid M where
-  carrier := _root_.closure (s : Set M)
-  one_mem' := _root_.subset_closure s.one_mem
-  mul_mem' ha hb := s.top_closure_mul_self_subset ⟨_, ha, _, hb, rfl⟩
+def Submonoid.topologicalClosure : ClosureOperator (Submonoid M) := .mk₂
+  (fun s ↦ { carrier := _root_.closure s
+             one_mem' := _root_.subset_closure s.one_mem
+             mul_mem' ha hb := s.top_closure_mul_self_subset ⟨_, ha, _, hb, rfl⟩})
+  (fun _ ↦ _root_.subset_closure)
+  (fun _ _ h ↦ closure_minimal h isClosed_closure)
 
 @[to_additive]
 theorem Submonoid.coe_topologicalClosure (s : Submonoid M) :