countable is measurable (#1381)

* countable is measurable --------- Co-authored-by: IshiguroYoshihiro <[email protected]>
math-comp · Nov 6, 2024 · 0df1797 · 0df1797
1 parent 1673e6e
commit 0df1797
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -67,6 +67,8 @@
 - in file `separation_axioms.v`,
   + new lemma `sigT_hausdorff`.
 
+- in `measure.v`:
+  + lemma `countable_measurable`
 
 ### Changed
 

diff --git a/theories/measure.v b/theories/measure.v
@@ -1367,6 +1367,17 @@ Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed.
 
 End sigmaring_lemmas.
 
+Lemma countable_measurable d (T : sigmaRingType d) (A : set T) :
+  (forall t : T, measurable [set t]) -> countable A -> measurable A.
+Proof.
+move=> m1; have [->//|/set0P[r Ar]/countable_injP[f injf]] := eqVneq A set0.
+rewrite -(injpinv_image (cst r) injf).
+rewrite [X in _ X](_ : _ = \bigcup_(x in f @` A) [set 'pinv_(cst r) A f x]).
+  by apply: bigcup_measurable => _ /= [s As <-].
+by rewrite eqEsubset; split=> [_ [_ [s As <-]] <-|_ [_ [s As <-]] ->];
+  exists (f s).
+Qed.
+
 Section sigma_ring_lambda_system.
 Context d (T : sigmaRingType d).