G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ HasBasis (FilterBasis.filter toFilterBasis) (fun V => V ∈ B) id
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ HasBasis (𝓝 1) (fun V => V ∈ B) id
rw [B.nhds_one_eq]
no goals
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ HasBasis (FilterBasis.filter toFilterBasis) (fun V => V ∈ B) id
exact B.toFilterBasis.hasBasis