M : Type ?u.165207
α : Type u_1
β : Type ?u.165213
Γ : Type ?u.165216
inst✝⁶ : Group Γ
T : Type ?u.165222
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
h : c • s ∈ 𝓝 (c • x)
⊢ s ∈ 𝓝 x
M : Type ?u.165207
α : Type u_1
β : Type ?u.165213
Γ : Type ?u.165216
inst✝⁶ : Group Γ
T : Type ?u.165222
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
⊢ c • s ∈ 𝓝 (c • x) ↔ s ∈ 𝓝 x
refine' ⟨fun h => _, fun h => set_smul_mem_nhds_smul h hc⟩
M : Type ?u.165207
α : Type u_1
β : Type ?u.165213
Γ : Type ?u.165216
inst✝⁶ : Group Γ
T : Type ?u.165222
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
h : c • s ∈ 𝓝 (c • x)
⊢ c⁻¹ • c • s ∈ 𝓝 (c⁻¹ • c • x)
M : Type ?u.165207
α : Type u_1
β : Type ?u.165213
Γ : Type ?u.165216
inst✝⁶ : Group Γ
T : Type ?u.165222
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
h : c • s ∈ 𝓝 (c • x)
⊢ s ∈ 𝓝 x
rw [← inv_smul_smul₀ hc x, ← inv_smul_smul₀ hc s]
no goals
M : Type ?u.165207
α : Type u_1
β : Type ?u.165213
Γ : Type ?u.165216
inst✝⁶ : Group Γ
T : Type ?u.165222
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
h : c • s ∈ 𝓝 (c • x)
⊢ c⁻¹ • c • s ∈ 𝓝 (c⁻¹ • c • x)
exact set_smul_mem_nhds_smul h (inv_ne_zero hc)