G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ N B 1 = FilterBasis.filter toFilterBasis
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ 𝓝 1 = FilterBasis.filter toFilterBasis
rw [B.nhds_eq]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ map (fun y => y) (FilterBasis.filter toFilterBasis) = FilterBasis.filter toFilterBasis
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ N B 1 = FilterBasis.filter toFilterBasis
simp only [N, one_mul]
no goals
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ map (fun y => y) (FilterBasis.filter toFilterBasis) = FilterBasis.filter toFilterBasis
exact map_id