feat(Topology/Algebra): add smul_mem_nhds_smul (#15563)

urkud · urkud · commit 1339db17c9ab · 2024-08-09T02:03:51.000Z
- add `smul_mem_nhds_smul_iff` and `smul_mem_nhds_smul`, deprecate `smul_mem_nhds`;
- move 3 lemmas up in the import graph;
- add `smul_mem_nhds_self`;
- rename `set_smul_mem_nhds_smul_iff` to `smul_mem_nhds_smul_iff₀`, deprecate the old lemma;
- similarly with `set_smul_mem_nhds_smul` and `smul_mem_nhds_smul₀`;
diff --git a/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean b/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean
@@ -63,8 +63,7 @@ def LinearMap.clmOfExistsBoundedImage (f : E →ₗ[𝕜] F)
         _ ⊆ f ⁻¹' U := by rw [inv_smul_smul₀ x_ne _]
     -- Using this inclusion, it suffices to show that `x⁻¹ • V` is in `𝓝 0`, which is trivial.
     refine mem_of_superset ?_ this
-    convert set_smul_mem_nhds_smul hV (inv_ne_zero x_ne)
-    exact (smul_zero _).symm⟩
+    rwa [set_smul_mem_nhds_zero_iff (inv_ne_zero x_ne)]⟩
 
 theorem LinearMap.clmOfExistsBoundedImage_coe {f : E →ₗ[𝕜] F}
     {h : ∃ V ∈ 𝓝 (0 : E), Bornology.IsVonNBounded 𝕜 (f '' V)} :
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@@ -776,9 +776,9 @@ theorem measure_isHaarMeasure_eq_smul_of_isEverywherePos [LocallyCompactSpace G]
       have C : Set.Countable (support fun (i : m) ↦ ρ (s ∩ (i : G) • k)) :=
         Summable.countable_support_ennreal this.ne
       have : support (fun (i : m) ↦ ρ (s ∩ (i : G) • k)) = univ := by
-        apply eq_univ_iff_forall.2 (fun i ↦ ?_)
-        apply ne_of_gt (hρ (i : G) (hms i.2) _ _)
-        exact inter_mem_nhdsWithin s (by simpa using smul_mem_nhds (i : G) k_mem)
+        refine eq_univ_iff_forall.2 fun i ↦ ?_
+        refine ne_of_gt (hρ (i : G) (hms i.2) _ ?_)
+        exact inter_mem_nhdsWithin s (by simpa)
       rw [this] at C
       have : Countable m := countable_univ_iff.mp C
       exact to_countable m
diff --git a/Mathlib/Topology/Algebra/ConstMulAction.lean b/Mathlib/Topology/Algebra/ConstMulAction.lean
@@ -202,7 +202,7 @@ theorem continuous_const_smul_iff (c : G) : (Continuous fun x => c • f x) ↔
 
 /-- The homeomorphism given by scalar multiplication by a given element of a group `Γ` acting on
   `T` is a homeomorphism from `T` to itself. -/
-@[to_additive]
+@[to_additive (attr := simps!)]
 def Homeomorph.smul (γ : G) : α ≃ₜ α where
   toEquiv := MulAction.toPerm γ
   continuous_toFun := continuous_const_smul γ
@@ -240,6 +240,29 @@ theorem Dense.smul (c : G) {s : Set α} (hs : Dense s) : Dense (c • s) := by
 theorem interior_smul (c : G) (s : Set α) : interior (c • s) = c • interior s :=
   ((Homeomorph.smul c).image_interior s).symm
 
+@[to_additive]
+theorem IsOpen.smul_left {s : Set G} {t : Set α} (ht : IsOpen t) : IsOpen (s • t) := by
+  rw [← iUnion_smul_set]
+  exact isOpen_biUnion fun a _ => ht.smul _
+
+@[to_additive]
+theorem subset_interior_smul_right {s : Set G} {t : Set α} : s • interior t ⊆ interior (s • t) :=
+  interior_maximal (Set.smul_subset_smul_left interior_subset) isOpen_interior.smul_left
+
+@[to_additive (attr := simp)]
+theorem smul_mem_nhds_smul_iff {t : Set α} (g : G) {a : α} : g • t ∈ 𝓝 (g • a) ↔ t ∈ 𝓝 a :=
+  (Homeomorph.smul g).openEmbedding.image_mem_nhds
+
+@[to_additive] alias ⟨_, smul_mem_nhds_smul⟩ := smul_mem_nhds_smul_iff
+
+@[to_additive (attr := deprecated (since := "2024-08-06"))]
+alias smul_mem_nhds := smul_mem_nhds_smul
+
+@[to_additive (attr := simp)]
+theorem smul_mem_nhds_self [TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G} :
+    g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1 := by
+  rw [← smul_mem_nhds_smul_iff g⁻¹]; simp
+
 end Group
 
 section GroupWithZero
@@ -346,38 +369,35 @@ variable [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul
 
 nonrec theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) :
     Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ tendsto_const_smul_iff u
+  tendsto_const_smul_iff hc.unit
 
 variable [TopologicalSpace β] {f : β → α} {b : β} {c : M} {s : Set β}
 
 nonrec theorem continuousWithinAt_const_smul_iff (hc : IsUnit c) :
     ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ continuousWithinAt_const_smul_iff u
+  continuousWithinAt_const_smul_iff hc.unit
 
 nonrec theorem continuousOn_const_smul_iff (hc : IsUnit c) :
     ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ continuousOn_const_smul_iff u
+  continuousOn_const_smul_iff hc.unit
 
 nonrec theorem continuousAt_const_smul_iff (hc : IsUnit c) :
     ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ continuousAt_const_smul_iff u
+  continuousAt_const_smul_iff hc.unit
 
 nonrec theorem continuous_const_smul_iff (hc : IsUnit c) :
     (Continuous fun x => c • f x) ↔ Continuous f :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ continuous_const_smul_iff u
+  continuous_const_smul_iff hc.unit
 
 nonrec theorem isOpenMap_smul (hc : IsUnit c) : IsOpenMap fun x : α => c • x :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ isOpenMap_smul u
+  isOpenMap_smul hc.unit
 
 nonrec theorem isClosedMap_smul (hc : IsUnit c) : IsClosedMap fun x : α => c • x :=
-  let ⟨u, hu⟩ := hc
-  hu ▸ isClosedMap_smul u
+  isClosedMap_smul hc.unit
+
+nonrec theorem smul_mem_nhds_smul_iff (hc : IsUnit c) {s : Set α} {a : α} :
+    c • s ∈ 𝓝 (c • a) ↔ s ∈ 𝓝 a :=
+  smul_mem_nhds_smul_iff hc.unit
 
 end IsUnit
 
@@ -474,19 +494,20 @@ section MulAction
 variable {G₀ : Type*} [GroupWithZero G₀] [MulAction G₀ α] [TopologicalSpace α]
   [ContinuousConstSMul G₀ α]
 
--- Porting note: generalize to a group action + `IsUnit`
-/-- Scalar multiplication preserves neighborhoods. -/
-theorem set_smul_mem_nhds_smul {c : G₀} {s : Set α} {x : α} (hs : s ∈ 𝓝 x) (hc : c ≠ 0) :
-    c • s ∈ 𝓝 (c • x : α) := by
-  rw [mem_nhds_iff] at hs ⊢
-  obtain ⟨U, hs', hU, hU'⟩ := hs
-  exact ⟨c • U, Set.smul_set_mono hs', hU.smul₀ hc, Set.smul_mem_smul_set hU'⟩
+/-- Scalar multiplication by a nonzero scalar preserves neighborhoods. -/
+theorem smul_mem_nhds_smul_iff₀ {c : G₀} {s : Set α} {x : α} (hc : c ≠ 0) :
+    c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x :=
+  smul_mem_nhds_smul_iff (Units.mk0 c hc)
 
-theorem set_smul_mem_nhds_smul_iff {c : G₀} {s : Set α} {x : α} (hc : c ≠ 0) :
-    c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x := by
-  refine ⟨fun h => ?_, fun h => set_smul_mem_nhds_smul h hc⟩
-  rw [← inv_smul_smul₀ hc x, ← inv_smul_smul₀ hc s]
-  exact set_smul_mem_nhds_smul h (inv_ne_zero hc)
+@[deprecated (since := "2024-08-06")]
+alias set_smul_mem_nhds_smul_iff := smul_mem_nhds_smul_iff₀
+
+alias ⟨_, smul_mem_nhds_smul₀⟩ := smul_mem_nhds_smul_iff₀
+
+@[deprecated  smul_mem_nhds_smul₀ (since := "2024-08-06")]
+theorem set_smul_mem_nhds_smul {c : G₀} {s : Set α} {x : α} (hs : s ∈ 𝓝 x) (hc : c ≠ 0) :
+    c • s ∈ 𝓝 (c • x : α) :=
+  smul_mem_nhds_smul₀ hc hs
 
 end MulAction
 
@@ -497,7 +518,7 @@ variable {G₀ : Type*} [GroupWithZero G₀] [AddMonoid α] [DistribMulAction G
 
 theorem set_smul_mem_nhds_zero_iff {s : Set α} {c : G₀} (hc : c ≠ 0) :
     c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α) := by
-  refine Iff.trans ?_ (set_smul_mem_nhds_smul_iff hc)
+  refine Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)
   rw [smul_zero]
 
 end DistribMulAction
diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -1047,20 +1047,6 @@ section ContinuousConstSMul
 variable [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α}
   {t : Set β}
 
-@[to_additive]
-theorem IsOpen.smul_left (ht : IsOpen t) : IsOpen (s • t) := by
-  rw [← iUnion_smul_set]
-  exact isOpen_biUnion fun a _ => ht.smul _
-
-@[to_additive]
-theorem subset_interior_smul_right : s • interior t ⊆ interior (s • t) :=
-  interior_maximal (Set.smul_subset_smul_left interior_subset) isOpen_interior.smul_left
-
-@[to_additive]
-theorem smul_mem_nhds (a : α) {x : β} (ht : t ∈ 𝓝 x) : a • t ∈ 𝓝 (a • x) := by
-  rcases mem_nhds_iff.1 ht with ⟨u, ut, u_open, hu⟩
-  exact mem_nhds_iff.2 ⟨a • u, smul_set_mono ut, u_open.smul a, smul_mem_smul_set hu⟩
-
 variable [TopologicalSpace α]
 
 @[to_additive]
@@ -1138,8 +1124,7 @@ theorem subset_interior_mul : interior s * interior t ⊆ interior (s * t) :=
 
 @[to_additive]
 theorem singleton_mul_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : {a} * s ∈ 𝓝 (a * b) := by
-  have := smul_mem_nhds a h
-  rwa [← singleton_smul] at this
+  rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]
 
 @[to_additive]
 theorem singleton_mul_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : {a} * s ∈ 𝓝 a := by
@@ -1153,8 +1138,8 @@ variable [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {
 
 @[to_additive]
 theorem IsOpen.mul_right (hs : IsOpen s) : IsOpen (s * t) := by
-  rw [← iUnion_op_smul_set]
-  exact isOpen_biUnion fun a _ => hs.smul _
+  rw [← image_op_smul]
+  exact hs.smul_left
 
 @[to_additive]
 theorem subset_interior_mul_left : interior s * t ⊆ interior (s * t) :=
@@ -1166,8 +1151,8 @@ theorem subset_interior_mul' : interior s * interior t ⊆ interior (s * t) :=
 
 @[to_additive]
 theorem mul_singleton_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : s * {a} ∈ 𝓝 (b * a) := by
-  simp only [← iUnion_op_smul_set, mem_singleton_iff, iUnion_iUnion_eq_left]
-  exact smul_mem_nhds _ h
+  rw [mul_singleton]
+  exact smul_mem_nhds_smul (op a) h
 
 @[to_additive]
 theorem mul_singleton_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : s * {a} ∈ 𝓝 a := by
diff --git a/Mathlib/Topology/Algebra/Group/OpenMapping.lean b/Mathlib/Topology/Algebra/Group/OpenMapping.lean
@@ -45,10 +45,8 @@ theorem smul_singleton_mem_nhds_of_sigmaCompact
   if `V` is small enough. -/
   obtain ⟨V, V_mem, V_closed, V_symm, VU⟩ : ∃ V ∈ 𝓝 (1 : G), IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U :=
     exists_closed_nhds_one_inv_eq_mul_subset hU
-  obtain ⟨s, s_count, hs⟩ : ∃ (s : Set G), s.Countable ∧ ⋃ g ∈ s, g • V = univ := by
-    apply countable_cover_nhds_of_sigma_compact (fun g ↦ ?_)
-    convert smul_mem_nhds g V_mem
-    simp only [smul_eq_mul, mul_one]
+  obtain ⟨s, s_count, hs⟩ : ∃ (s : Set G), s.Countable ∧ ⋃ g ∈ s, g • V = univ :=
+    countable_cover_nhds_of_sigma_compact fun _ ↦ by simpa
   let K : ℕ → Set G := compactCovering G
   let F : ℕ × s → Set X := fun p ↦ (K p.1 ∩ (p.2 : G) • V) • ({x} : Set X)
   obtain ⟨⟨n, ⟨g, hg⟩⟩, hi⟩ : ∃ i, (interior (F i)).Nonempty := by
diff --git a/Mathlib/Topology/Maps/Basic.lean b/Mathlib/Topology/Maps/Basic.lean
@@ -559,6 +559,10 @@ theorem of_comp (f : X → Y) (hg : OpenEmbedding g)
 theorem of_isEmpty [IsEmpty X] (f : X → Y) : OpenEmbedding f :=
   openEmbedding_of_embedding_open (.of_subsingleton f) (IsOpenMap.of_isEmpty f)
 
+theorem image_mem_nhds {f : X → Y} (hf : OpenEmbedding f) {s : Set X} {x : X} :
+    f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x := by
+  rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.inj]
+
 end OpenEmbedding
 
 end OpenEmbedding
