class PiBase.HasCofiniteTopology (X : Type u) [TopologicalSpace X] : Prop

• open_iff_cofinite (s : Set X) : IsOpen s ↔ s.Nonempty → sᶜ.Finite