closed_bigcup (#991)

math-comp · Jul 31, 2023 · 902670c · 902670c
1 parent 84fcbd6
commit 902670c
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git 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
@@ -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.