ι : Type ?u.6011
α : Type ?u.6014
β : Type ?u.6017
l : Filter α
⊢ cofinite ≤ atTop
ι : Type ?u.6011
α : Type ?u.6014
β : Type ?u.6017
l : Filter α
⊢ cofinite = atTop
refine' le_antisymm _ atTop_le_cofinite
ι : Type ?u.6011
α : Type ?u.6014
β : Type ?u.6017
l : Filter α
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite
ι : Type ?u.6011
α : Type ?u.6014
β : Type ?u.6017
l : Filter α
⊢ cofinite ≤ atTop
refine' atTop_basis.ge_iff.2 fun N _ => _
no goals
ι : Type ?u.6011
α : Type ?u.6014
β : Type ?u.6017
l : Filter α
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite
simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N