M : Type ?u.62639
α : Type u_1
β : Type ?u.62645
G : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s✝ : Set β
c : G
s : Set α
hs : closure s = univ
⊢ closure (c • s) = univ
M : Type ?u.62639
α : Type u_1
β : Type ?u.62645
G : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s✝ : Set β
c : G
s : Set α
hs : Dense s
⊢ Dense (c • s)
rw [dense_iff_closure_eq] at hs ⊢
no goals
M : Type ?u.62639
α : Type u_1
β : Type ?u.62645
G : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s✝ : Set β
c : G
s : Set α
hs : closure s = univ
⊢ closure (c • s) = univ
rw [closure_smul, hs, smul_set_univ]