Merge pull request #332 from math-comp/bigcup_distr_fix

minor lemma generalization
math-comp · Mar 4, 2021 · e135fce · e135fce
2 parents d3cee2b + 6de9d78
commit e135fce
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -54,6 +54,9 @@
 - in `classical_sets.v`:
   + generalization and change of `trivIset` (and thus lemmas `trivIset_bigUI` and `trivIset_setI`)
 
+- in `classical_sets.v`:
+  + `bigcup_distrr`, `bigcup_distrl` generalized
+
 ### Renamed
 
 - in `normedtype.v`, `bounded_on` -> `bounded_near`

diff --git a/theories/classical_sets.v b/theories/classical_sets.v
@@ -740,15 +740,17 @@ rewrite predeqE => t; split => [[[|m] _ At]|[At|[i _ At]]].
   by exists i.+1 => //; rewrite -addSnnS.
 Qed.
 
-Lemma bigcup_distrr F A : A `&` \bigcup_i (F i) = \bigcup_i (A `&` F i).
+Lemma bigcup_distrr F (P : set nat) A :
+  A `&` \bigcup_(i in P) (F i) = \bigcup_(i in P) (A `&` F i).
 Proof.
-rewrite predeqE => t; split => [[At [k _ ?]]|[k _ [At ?]]];
+rewrite predeqE => t; split => [[At [k ? ?]]|[k ? [At ?]]];
   by [exists k |split => //; exists k].
 Qed.
 
-Lemma bigcup_distrl F A : \bigcup_i F i `&` A = \bigcup_i (F i `&` A).
+Lemma bigcup_distrl F (P : set nat) A :
+  \bigcup_(i in P) F i `&` A = \bigcup_(i in P) (F i `&` A).
 Proof.
-by rewrite predeqE => t; split => [[[n _ Ant ?]]|[n _ [Ant ?]]];
+by rewrite predeqE => t; split => [[[n ? Ant ?]]|[n ? [Ant ?]]];
   [exists n|split => //; exists n].
 Qed.