G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ HasBasis (N B x₀) (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ HasBasis (𝓝 x₀) (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
rw [B.nhds_eq]
no goals
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ HasBasis (N B x₀) (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
apply B.hasBasis