From dd94a22240c44362c47e185c7c3840369c9f74a1 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 5 Nov 2024 18:37:38 +0900
Subject: [PATCH] countable is measurable

Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
---
 CHANGELOG_UNRELEASED.md     |  2 ++
 theories/lebesgue_measure.v | 10 ++++++++++
 2 files changed, 12 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2b9213098..1885db7df 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -67,6 +67,8 @@
 - in file `separation_axioms.v`,
   + new lemma `sigT_hausdorff`.
 
+- in `lebesgue_measure.v`:
+  + lemma `countable_measurable`
 
 ### Changed
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index e658b9a26..0cfca4951 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -215,6 +215,16 @@ by apply: sub_sigma_algebra; exact/is_ocitv.
 Qed.
 #[local] Hint Resolve measurable_set1 : core.
 
+Lemma countable_measurable (A : set R) : countable A -> measurable A.
+Proof.
+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.
+
 Lemma measurable_itv (i : interval R) : measurable [set` i].
 Proof.
 have moc (a b : R) : measurable `]a, b].