Merge pull request #1433 from affeldt-aist/measure_20241210

minor generalization

CHANGELOG_UNRELEASED.md

@@ -33,7 +33,10 @@
   + lemma `integral_measure_add`
 
 - in `probability.v`
-  + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed)
+  + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed)
+
+- in `measure.v`:
+  + lemma `countable_bigcupT_measurable`
 
 - in file `realfun.v`:
   + lemma `cvg_nbhsP`

classical/classical_sets.v

@@ -2602,6 +2602,7 @@ Proof.
 by apply: qcanon; elim/eqPchoice; elim/choicePpointed => [[T F]|T];
    [left; exists (Empty.Pack F) | right; exists T].
 Qed.
+
 Lemma Ppointed : quasi_canonical Type pointedType.
 Proof.
 by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T];

theories/measure.v

@@ -1390,13 +1390,20 @@ Qed.
 
 End sigma_ring_lambda_system.
 
-Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) :
+Lemma countable_bigcupT_measurable d (T : sigmaRingType d) U
+    (F : U -> set T) : countable [set: U] ->
   (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
 Proof.
-move=> Fm; have /ppcard_eqP[f] := card_rat.
-by rewrite (reindex_bigcup f^-1%FUN setT)//=; exact: bigcupT_measurable.
+elim/Ppointed: U => U in F *; first by move=> *; rewrite empty_eq0 bigcup0.
+move=> /countable_bijP[B] /ppcard_eqP[f] Fm.
+rewrite (reindex_bigcup f^-1%FUN setT)//=; first exact: bigcupT_measurable.
+exact: (@subl_surj _ _ B).
 Qed.
 
+Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) :
+  (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
+Proof. exact/countable_bigcupT_measurable. Qed.
+
 Section measurable_lemmas.
 Context d (T : measurableType d).
 Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat).