minor lemma generalization

math-comp · Feb 10, 2021 · 6de9d78 · 6de9d78
1 parent a21bb29
commit 6de9d78
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
@@ -35,6 +35,9 @@
 - in `reals.v`:
   + `floor_ge0` generalized and renamed to `floorR_ge_int`
 
+- 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
@@ -728,15 +728,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.