From 4b9af2678a20b68318265ed72b25b6fa4c6c8585 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 10 Dec 2024 18:25:38 +0900
Subject: [PATCH 1/2] minor generalization

---
 CHANGELOG_UNRELEASED.md    |  5 ++++-
 classical/classical_sets.v |  1 +
 theories/measure.v         | 15 +++++++++++++--
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 56017a4e2..e5a20cd80 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/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`
 
 ### Changed
 
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index e4dc9adeb..e5e7579d2 100644
--- a/classical/classical_sets.v
+++ b/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];
diff --git a/theories/measure.v b/theories/measure.v
index 691b79f9b..702cd1d65 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1390,11 +1390,22 @@ Qed.
 
 End sigma_ring_lambda_system.
 
+Lemma countable_bigcupT_measurable d (T : sigmaRingType d) (U : choiceType)
+    (F : U -> set T) : countable [set: U] ->
+  (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
+Proof.
+elim/choicePpointed: U => U in F *.
+  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.
-move=> Fm; have /ppcard_eqP[f] := card_rat.
-by rewrite (reindex_bigcup f^-1%FUN setT)//=; exact: bigcupT_measurable.
+apply: countable_bigcupT_measurable.
+by apply/countable_bijP; exists setT; exact: card_rat.
 Qed.
 
 Section measurable_lemmas.

From 2978c5403d225aa16fbb457cebdbdea4991619cf Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Wed, 18 Dec 2024 00:01:12 +0100
Subject: [PATCH 2/2] simplifications

---
 theories/measure.v | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/theories/measure.v b/theories/measure.v
index 702cd1d65..9b4e488c4 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1390,12 +1390,11 @@ Qed.
 
 End sigma_ring_lambda_system.
 
-Lemma countable_bigcupT_measurable d (T : sigmaRingType d) (U : choiceType)
+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.
-elim/choicePpointed: U => U in F *.
-  by move=> _ _; rewrite empty_eq0 bigcup0.
+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).
@@ -1403,10 +1402,7 @@ Qed.
 
 Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) :
   (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
-Proof.
-apply: countable_bigcupT_measurable.
-by apply/countable_bijP; exists setT; exact: card_rat.
-Qed.
+Proof. exact/countable_bigcupT_measurable. Qed.
 
 Section measurable_lemmas.
 Context d (T : measurableType d).