feat(analysis/*): generalize set_smul_mem_nhds_zero to topological …

…vector spaces (#12779)

The lemma holds for arbitrary topological vector spaces and has nothing to do with normed spaces.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/analysis/normed_space/pointwise.lean

@@ -87,24 +87,6 @@ begin
   simpa only [this, dist_eq_norm, add_sub_cancel', mem_closed_ball] using I,
 end
 
-lemma set_smul_mem_nhds_zero {s : set E} (hs : s ∈ 𝓝 (0 : E)) {c : 𝕜} (hc : c ≠ 0) :
-  c • s ∈ 𝓝 (0 : E) :=
-begin
-  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : 0 < ε), ball 0 ε ⊆ s := metric.mem_nhds_iff.1 hs,
-  have : c • ball (0 : E) ε ∈ 𝓝 (0 : E),
-  { rw [smul_ball hc, smul_zero],
-    exact ball_mem_nhds _ (mul_pos (by simpa using hc) εpos) },
-  exact filter.mem_of_superset this ((set_smul_subset_set_smul_iff₀ hc).2 hε)
-end
-
-lemma set_smul_mem_nhds_zero_iff (s : set E) {c : 𝕜} (hc : c ≠ 0) :
-  c • s ∈ 𝓝 (0 : E) ↔ s ∈ 𝓝(0 : E) :=
-begin
-  refine ⟨λ h, _, λ h, set_smul_mem_nhds_zero h hc⟩,
-  convert set_smul_mem_nhds_zero h (inv_ne_zero hc),
-  rw [smul_smul, inv_mul_cancel hc, one_smul],
-end
-
 /-- Any ball is the image of a ball centered at the origin under a shift. -/
 lemma vadd_ball_zero (x : E) (r : ℝ) : x +ᵥ ball 0 r = ball x r :=
 by rw [vadd_ball, vadd_eq_add, add_zero]

src/topology/algebra/const_mul_action.lean

@@ -375,3 +375,45 @@ begin
     simp only [image_smul, not_not, mem_set_of_eq, ne.def] at H,
     exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩ },
 end
+
+section nhds
+
+section mul_action
+
+variables {G₀ : Type*} [group_with_zero G₀] [mul_action G₀ α]
+  [topological_space α] [has_continuous_const_smul G₀ α]
+
+/-- Scalar multiplication preserves neighborhoods. -/
+lemma set_smul_mem_nhds_smul {c : G₀} {s : set α} {x : α} (hs : s ∈ 𝓝 x) (hc : c ≠ 0) :
+  c • s ∈ 𝓝 (c • x : α) :=
+begin
+  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'⟩,
+end
+
+lemma set_smul_mem_nhds_smul_iff {c : G₀} {s : set α} {x : α} (hc : c ≠ 0) :
+  c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x :=
+begin
+  refine ⟨λ h, _, λ 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),
+end
+
+end mul_action
+
+section distrib_mul_action
+
+variables {G₀ : Type*} [group_with_zero G₀] [add_monoid α] [distrib_mul_action G₀ α]
+  [topological_space α] [has_continuous_const_smul G₀ α]
+
+lemma set_smul_mem_nhds_zero_iff {s : set α} {c : G₀} (hc : c ≠ 0) :
+  c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α) :=
+begin
+  refine iff.trans _ (set_smul_mem_nhds_smul_iff hc),
+  rw smul_zero,
+end
+
+end distrib_mul_action
+
+end nhds