ι : Type ?u.2270
α : Type u_1
β : Type ?u.2276
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite (sᶜ)
⊢ s ∈ l
ι : Type ?u.2270
α : Type u_1
β : Type ?u.2276
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
refine' ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => _⟩
ι : Type ?u.2270
α : Type u_1
β : Type ?u.2276
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite (sᶜ)
⊢ ∀ (i : α), i ∈ sᶜ → {i}ᶜ ∈ l
ι : Type ?u.2270
α : Type u_1
β : Type ?u.2276
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite (sᶜ)
⊢ s ∈ l
rw [← compl_compl s, ← biUnion_of_singleton (sᶜ), compl_iUnion₂, Filter.biInter_mem hs]
no goals
ι : Type ?u.2270
α : Type u_1
β : Type ?u.2276
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite (sᶜ)
⊢ ∀ (i : α), i ∈ sᶜ → {i}ᶜ ∈ l
exact fun x _ => h x