no goals
α : Type u
β : Type v
γ : Type ?u.17786
δ : Type ?u.17789
ε : Type ?u.17792
ζ : Type ?u.17795
s : Set (CofiniteTopology α)
⊢ IsClosed s ↔ s = univ ∨ Set.Finite s
simp only [← isOpen_compl_iff, isOpen_iff', compl_compl, compl_empty_iff]