diff --git a/src/topology/compacts.lean b/src/topology/compacts.lean
index 7ed377bf1ced6..6d2010737a052 100644
--- a/src/topology/compacts.lean
+++ b/src/topology/compacts.lean
@@ -27,6 +27,9 @@ namespace topological_space
 /-- The type of closed subsets of a topological space. -/
 def closeds := {s : set α // is_closed s}
 
+/-- The type of closed subsets is inhabited, with default element the empty set. -/
+instance : inhabited (closeds α) := ⟨⟨∅, is_closed_empty ⟩⟩
+
 /-- The compact sets of a topological space. See also `nonempty_compacts`. -/
 def compacts : Type* := { s : set α // is_compact s }
 
@@ -35,6 +38,11 @@ non-emptiness will be useful in metric spaces, as we will be able to put
 a distance (and not merely an edistance) on this space. -/
 def nonempty_compacts := {s : set α // s.nonempty ∧ is_compact s}
 
+/-- In an inhabited space, the type of nonempty compact subsets is also inhabited, with
+default element the singleton set containing the default element. -/
+instance nonempty_compacts_inhabited [inhabited α] : inhabited (nonempty_compacts α) :=
+⟨⟨{default α}, singleton_nonempty (default α), compact_singleton ⟩⟩
+
 /-- The compact sets with nonempty interior of a topological space. See also `compacts` and
   `nonempty_compacts`. -/
 @[nolint has_inhabited_instance]