countable is measurable

Co-authored-by: IshiguroYoshihiro <[email protected]>
math-comp · Nov 5, 2024 · dd94a22 · dd94a22
1 parent d26b17b
commit dd94a22
Show file tree

Hide file tree

Showing 2 changed files with 12 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 `lebesgue_measure.v`:
+  + lemma `countable_measurable`
 
 ### Changed
 

diff --git 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].