α : Type u_1
β : Type ?u.111166
γ : Type ?u.111169
ι : Type ?u.111172
ι' : Sort ?u.111175
a : α
⊢ IsCountablyGenerated (𝓟 {a})
α : Type u_1
β : Type ?u.111166
γ : Type ?u.111169
ι : Type ?u.111172
ι' : Sort ?u.111175
a : α
⊢ IsCountablyGenerated (pure a)
rw [← principal_singleton]
no goals
α : Type u_1
β : Type ?u.111166
γ : Type ?u.111169
ι : Type ?u.111172
ι' : Sort ?u.111175
a : α
⊢ IsCountablyGenerated (𝓟 {a})
exact isCountablyGenerated_principal _