lemma generalization

CHANGELOG_UNRELEASED.md

@@ -98,8 +98,6 @@
   + lemma `lebesgue_measure_set1`
   + lemma `lebesgue_measure_itv`
   + lemma `lebesgue_measure_rat`
-- in file `classical_sets.v`:
-  + lemma `bigcup_oppr`
 - in file `set_interval.v`:
   + lemma `opp_itv_infty_bnd`
 
@@ -117,6 +115,8 @@
   + change the notation `\int_`
 - in `set_interval.v`:
   + generalize `opp_itvoo` to `opp_itv_bnd_bnd`
+- in `classical_sets.v`:
+  + lemma `some_bigcup` generalized and renamed to `image_bigcup`
 
 ### Renamed
 

theories/classical_sets.v

@@ -1411,11 +1411,11 @@ apply: setC_inj; rewrite setC_bigcup setCK.
 by apply: eq_bigcapr => ?; rewrite setCK.
 Qed.
 
-Lemma some_bigcup P F :
-  some @` (\bigcup_(i in P) (F i)) = \bigcup_(i in P) some @` F i.
+Lemma image_bigcup rT P F (f : T -> rT) :
+  f @` (\bigcup_(i in P) (F i)) = \bigcup_(i in P) f @` F i.
 Proof.
-apply/seteqP; split; last by move=> _ [i ? [x ? <-]]; exists x => //; exists i.
-by move=> _ [x [i ? ?] <-]; exists i => //; exists x.
+apply/seteqP; split=> [_/= [x [i Pi Fix <-]]|]; first by exists i.
+by move=> _ [i Pi [x Fix <-]]; exists x => //; exists i.
 Qed.
 
 Lemma some_bigcap P F : some @` (\bigcap_(i in P) (F i)) =
@@ -2703,13 +2703,6 @@ rewrite -Order.TotalTheory.ltNge => kn.
 by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)).
 Qed.
 
-Lemma bigcup_oppr (R : zmodType) (I : Type) (F : I -> set R) :
-  \bigcup_i (-%R @` F i) = -%R @` \bigcup_i F i.
-Proof.
-by apply/seteqP; split=> [_ [i _/= [r Fir <-]]|x/= [r [i _ Fir <-]]];
-  [exists r => //; exists i | exists i].
-Qed.
-
 (** ** Intersection of classes of set *)
 
 Definition meets T (F G : set (set T)) :=

theories/lebesgue_measure.v

@@ -565,7 +565,7 @@ Lemma itv_open_bnd_bigcup (R : realType) b (r s : R) :
   \bigcup_n [set` Interval (BLeft (s + n.+1%:R^-1)) (BSide b r)].
 Proof.
 have /(congr1 (fun x => -%R @` x)) := itv_bnd_open_bigcup (~~ b) (- r) (- s).
-rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite -bigcup_oppr.
+rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite image_bigcup.
 apply eq_bigcupr => k _; apply/seteqP; split=> [_/= [y ysr] <-|x/= xsr].
   by rewrite oppr_itv/= opprD.
 by exists (- x); rewrite ?oppr_itv//= opprK// negbK opprB opprK addrC.
@@ -588,7 +588,7 @@ Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
   \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)].
 Proof.
 have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x).
-rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite -bigcup_oppr.
+rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup.
 apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb].
    by rewrite oppr_itv/= opprB addrC.
 by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK].