case intro
α : Type u_1
β : Type ?u.110343
γ : Type ?u.110346
ι : Type ?u.110349
ι' : Sort ?u.110352
x : ℕ → Set α
⊢ IsCountablyGenerated (⨅ (i : ℕ), 𝓟 (x i))
α : Type u_1
β : Type ?u.110343
γ : Type ?u.110346
ι : Type ?u.110349
ι' : Sort ?u.110352
f : Filter α
h : ∃ x, f = ⨅ (i : ℕ), 𝓟 (x i)
⊢ IsCountablyGenerated f
rcases h with ⟨x, rfl⟩
no goals
case intro
α : Type u_1
β : Type ?u.110343
γ : Type ?u.110346
ι : Type ?u.110349
ι' : Sort ?u.110352
x : ℕ → Set α
⊢ IsCountablyGenerated (⨅ (i : ℕ), 𝓟 (x i))
apply isCountablyGenerated_seq