no goals
α : Type u
β : Type v
γ : Type ?u.17451
δ : Type ?u.17454
ε : Type ?u.17457
ζ : Type ?u.17460
s : Set (CofiniteTopology α)
⊢ IsOpen s ↔ s = ∅ ∨ Set.Finite (sᶜ)
simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]