restore infinite_set_fset

CHANGELOG_UNRELEASED.md

@@ -91,9 +91,6 @@
   + lemmas `nneseries_ge0`, `is_cvg_nneseries_cond`, `is_cvg_npeseries_cond`,
     `is_cvg_nneseries`, `is_cvg_npeseries`, `nneseries_ge0`, `npeseries_le0`,
     `lee_nneseries`
-
-- in `cardinality.v`:
-  + lemma `infinite_set_fset`
 
 - in `normedtype.v`:
   + lemmas `not_near_at_rightP`, `not_near_at_leftP`

classical/cardinality.v

@@ -1004,27 +1004,21 @@ Qed.
 
 Lemma infinite_set_fset {T : choiceType} (A : set T) n :
   infinite_set A ->
-    exists B : {fset T}, [/\ [set` B] `<=` A, B != fset0 & (#|` B| >= n)%N].
+    exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N.
 Proof.
 elim/choicePpointed: T => T in A *; first by rewrite emptyE.
-move=> /infiniteP/ppcard_leP[f]; exists (fset_set [set f i | i in `I_n.+1]).
-rewrite fset_setK//; last exact: finite_image.
-split.
-- by apply: subset_trans (fun_image_sub f); exact: image_subset.
-- apply/eqP => /fsetP /(_ (f ord0)) => /(_ n).
-  rewrite !inE -falseE => <-.
-  rewrite in_fset_set//; last exact: finite_image.
-  by rewrite inE/=; exists 0.
-- rewrite fset_set_image// card_imfset//= fset_set_II/=.
-  by rewrite card_imfset//= ?size_enum_ord//; exact: val_inj.
+move=> /infiniteP/ppcard_leP[f]; exists (fset_set [set f i | i in `I_n]).
+  rewrite fset_setK//; last exact: finite_image.
+  by apply: subset_trans (fun_image_sub f); apply: image_subset.
+rewrite fset_set_image// card_imfset//= fset_set_II/=.
+by rewrite card_imfset//= ?size_enum_ord//; apply: val_inj.
 Qed.
 
 Lemma infinite_set_fsetP {T : choiceType} (A : set T) :
   infinite_set A <->
    forall n, exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N.
 Proof.
-split.
-  by move=> + n => /infinite_set_fset => /(_ n)[B [? ? ?]]; exists B.
+split; first by move=> ? ?; apply: infinite_set_fset.
 elim/choicePpointed: T => T in A *.
   move=> /(_ 1%N)[B _]; rewrite cardfs_gt0 => /fset0Pn[x xB].
   by have: [set` B] x by []; rewrite emptyE.

classical/mathcomp_extra.v

@@ -590,11 +590,13 @@ by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT.
 Qed.
 
 (* TODO: move to ssrnum *)
-Lemma ltr_sum {R : numDomainType} I (r : seq I) (F G : I -> R) :
-  (0 < size r)%N -> (forall i, F i < G i) ->
+Lemma ltr_sum {R : numDomainType} {I : eqType} (r : seq I) (F G : I -> R) :
+  (0 < size r)%N -> (forall i, i \in r -> F i < G i) ->
   \sum_(i <- r) F i < \sum_(i <- r) G i.
 Proof.
-elim: r => // h [|a t] ih ? FG.
-  by rewrite !big_cons !big_nil !addr0.
-by rewrite [ltLHS]big_cons [ltRHS]big_cons ltrD// ih.
+elim: r => // h [|a t] ih _ FG.
+  by rewrite !big_cons !big_nil !addr0 FG// mem_head.
+rewrite [ltLHS]big_cons [ltRHS]big_cons ltrD//.
+  by rewrite FG// mem_head.
+by rewrite ih// => i iat; rewrite FG// inE iat orbT.
 Qed.

theories/lebesgue_measure.v

@@ -2824,7 +2824,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
 have finite_set_F i : finite_set (F i).
   apply: contrapT.
   pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
-  move/(infinite_set_fset M) => [/= C [CsubFi _ McardC]].
+  move/(infinite_set_fset M) => [/= C CsubFi McardC].
   have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
             mu (\bigcup_(j in [set` C]) closure (B j)).
     rewrite (measure_bigcup _ [set` C])//; last 2 first.
@@ -3185,7 +3185,7 @@ have {}Hc : mu (\bigcup_(k in G) closure (B k) `\`
   by rewrite lteBlDr-?lteBlDl//; exact: muGSfin.
 have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num).
   pose M := `|ceil (fine (mu O) / r%:num)|.+1.
-  apply: contrapT => /infinite_set_fset /= /(_ M)[G0 [G0G'r _ MG0]].
+  apply: contrapT => /infinite_set_fset /= /(_ M)[G0 G0G'r MG0].
   have : mu O < mu (\bigcup_(k in bigB G r%:num) closure (B k)).
     apply: (@lt_le_trans _ _ (mu (\bigcup_(k in [set` G0]) closure (B k)))).
       rewrite bigcup_fset measure_fbigsetU//=; last 2 first.

theories/measure.v

@@ -2286,7 +2286,7 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A ->
   \esum_(i in A) \d_ i A = +oo :> \bar R.
 Proof.
 move=> infA; apply/eqyP => r r0.
-have [B [BA B0 Br]] := infinite_set_fset `|ceil r| infA.
+have [B BA Br] := infinite_set_fset `|ceil r| infA.
 apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E).
   by rewrite lee_fin natr_absz gtr0_norm -?ceil_gt0// ceil_ge.
 move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.