α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
a b : α
h : s ∈ 𝓝 b
⊢ MulOpposite.op a • s ∈ 𝓝 (b * a)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)
simp only [← iUnion_op_smul_set, mem_singleton_iff, iUnion_iUnion_eq_left]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
a b : α
h : s ∈ 𝓝 b
⊢ MulOpposite.op a • s ∈ 𝓝 (b * a)
exact smul_mem_nhds _ h