lemmas about cover

- from PR #371

Co-authored-by: Cyril Cohen <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `classical_sets.v`:
+  + lemmas `cover_restr`, `eqcover_r`
+
 ### Changed
 
 ### Renamed

theories/classical_sets.v

@@ -1505,6 +1505,27 @@ Qed.
 
 Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
 
+Lemma cover_restr T I D' D (F : I -> set T) :
+  D `<=` D' -> (forall i, D' i -> ~ D i -> F i = set0) ->
+  cover D F = cover D' F.
+Proof.
+move=> DD' D'DF; rewrite /cover eqEsubset; split=> [r [i Di Fit]|r [i D'i Fit]].
+- by have [D'i|] := pselect (D' i); [exists i | have := DD' _ Di].
+- by have [Di|Di] := pselect (D i); [exists i | move: Fit; rewrite (D'DF i)].
+Qed.
+
+Lemma eqcover_r T I D (F G : I -> set T) :
+  [set F i | i in D] = [set G i | i in D] ->
+  cover D F = cover D G.
+Proof.
+move=> FG.
+rewrite eqEsubset; split => [t [i Di Fit]|t [i Di Git]].
+  have [j Dj GF] : [set G i | i in D] (F i) by rewrite -FG /mkset; exists i.
+  by exists j => //; rewrite GF.
+have [j Dj GF] : [set F i | i in D] (G i) by rewrite FG /mkset; exists i.
+by exists j => //; rewrite GF.
+Qed.
+
 Definition partition T I D (F : I -> set T) (A : set T) :=
   [/\ cover D F = A, trivIset D F & forall i, D i -> F i !=set0].