α : Type u_1
β : Type ?u.166678
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : IsCountablyGenerated (𝓝 1)
⊢ IsCountablyGenerated (comap (fun x => x.snd / x.fst) (𝓝 1))
α : Type u_1
β : Type ?u.166678
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : IsCountablyGenerated (𝓝 1)
⊢ IsCountablyGenerated (𝓤 α)
rw [uniformity_eq_comap_nhds_one]
no goals
α : Type u_1
β : Type ?u.166678
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : IsCountablyGenerated (𝓝 1)
⊢ IsCountablyGenerated (comap (fun x => x.snd / x.fst) (𝓝 1))
exact Filter.comap.isCountablyGenerated _ _