diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 403e556f6f..b0e296f751 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -93,6 +93,9 @@
 - in `classical_sets.v`:
   + lemma `bigcup_bigcup`
 
+- in `topology.v`:
+  + lemma `closed_bigcup`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
diff --git a/theories/topology.v b/theories/topology.v
index e27bbaead7..530a9e145f 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2761,6 +2761,15 @@ move=> scF; rewrite big_seq.
 by elim/big_ind : _ => //; [exact: closed0|exact: closedU].
 Qed.
 
+Lemma closed_bigcup (T : topologicalType) (I : choiceType) (A : set I)
+    (F : I -> set T) :
+    finite_set A -> (forall i, A i -> closed (F i)) ->
+  closed (\bigcup_(i in A) F i).
+Proof.
+move=> finA cF; rewrite -bigsetU_fset_set//; apply: closed_bigsetU => i.
+by rewrite in_fset_set// inE; exact: cF.
+Qed.
+
 Section closure_lemmas.
 Variable T : topologicalType.
 Implicit Types E A B U : set T.