Merge pull request #249 from math-comp/bigcup_set1_fix

minor generalization
math-comp · Aug 11, 2020 · 048d9e9 · 048d9e9
2 parents ae360cd + d380da6
commit 048d9e9
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,9 @@
 
 ### Changed
 
+- in `classical_sets.v`:
+  + the index in `bigcup_set1` generalized from `nat` to some `Type`
+
 ### Renamed
 
 ### Removed

diff --git a/theories/classical_sets.v b/theories/classical_sets.v
@@ -529,8 +529,8 @@ Qed.
 Lemma setUDr T : right_distributive (@setU T) (@setI T).
 Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUDl. Qed.
 
-Lemma bigcup_set1 T (U : nat -> set T) n : \bigcup_(i in [set n]) U i = U n.
-Proof. by rewrite predeqE => t; split => [[m -> //]|Unt]; exists n. Qed.
+Lemma bigcup_set1 T V (U : V -> set T) v : \bigcup_(i in [set v]) U i = U v.
+Proof. by apply: eqEsubset => ? => [[] ? -> //|]; exists v. Qed.
 
 Lemma bigcapCU T (U : nat -> set T) : \bigcap_i (U i) = ~` (\bigcup_i (~` U i)).
 Proof.