Prove measurable_Borel_eq_topo_basis and use it for R and Rbar.

Lebesgue/measurable.v

@@ -26,7 +26,7 @@ From Coq Require Import Lia.
 From Coquelicot Require Import Hierarchy.
 
 Require Import UniformSpace_compl.
-Require Import Subset Subset_finite Subset_seq.
+Require Import Subset Subset_dec Subset_finite Subset_seq.
 Require Import Subset_system_base Subset_system_gen Subset_system.
 
 Open Scope nat_scope.
@@ -521,10 +521,30 @@ rewrite HB2; apply measurable_union_seq; intros n; apply measurable_gen, HB1.
 apply Incl_trans with open; now try apply measurable_gen.
 Qed.
 
-(* WIP.
 Lemma measurable_Borel_eq_topo_basis :
-  forall Idx B, @is_topo_basis E Idx B -> 
-*)
+  forall (B : nat -> E -> Prop),
+    is_topo_basis B -> (exists n0, empty (B n0)) ->
+    measurable_Borel = measurable (image B (@fullset nat)).
+Proof.
+intros B HB1 [n0 Hn0].
+apply is_topo_basis_to_Prop in HB1; destruct HB1 as [HB1a HB1b].
+apply measurable_Borel_gen_ext; intros A HA.
+induction HA as [n _]; apply HB1a; exists n; easy.
+exists (fun n => inter (Prop_cst (incl (B n) A)) (B n)); split.
+(* *)
+subset_unfold; intros n; case (in_dec (fun m => incl (B m) A) n); intros Hn.
+rewrite (subset_ext _ (B n)); easy.
+rewrite (subset_ext (fun x => _ /\ B n x) emptyset); try easy.
+rewrite empty_emptyset in Hn0; rewrite <- Hn0; easy.
+(* *)
+apply subset_ext; intros x; rewrite (HB1b A HA x); split.
+(* . *)
+intros [B' [[[n HB'1] HB'2] HB'3]].
+exists n; rewrite <- HB'1; split; easy.
+(* . *)
+intros [n [Hn1 Hn2]].
+exists (B n); repeat split; try easy; exists n; easy.
+Qed.
 
 End Borel_subsets.
 

Lebesgue/measurable_R.v

@@ -52,16 +52,18 @@ Qed.
 (* Lem 493 p. 71 *)
 Lemma measurable_R_Borel_eq_Qoo : measurable_Borel = measurable gen_R_Qoo.
 Proof.
-apply measurable_Borel_gen_ext; intros A HA.
+rewrite (measurable_Borel_eq_topo_basis topo_basis_R).
 (* *)
-induction HA; apply open_and; [apply open_gt | apply open_lt].
+f_equal; apply subset_ext_equiv; split; intros x Hx.
+induction Hx as [n _]; easy.
+induction Hx as [a b]; pose (n := bij_Q2N (a, b)).
+rewrite (subset_ext _ (topo_basis_R n)); try easy.
+unfold topo_basis_R, n; rewrite bij_NQ2N; easy.
 (* *)
-destruct (R_second_countable_alt A HA) as [P HP].
-exists (fun n => inter (Prop_cst (P n)) (topo_basis_R n)); split; try easy.
-subset_unfold; unfold topo_basis_R; intros n; case (in_dec P n); intros Hn.
-erewrite subset_ext; easy.
-rewrite subset_ext with (B := R_oo (Q2R 0) (Q2R 0)); try easy.
-R_interval_unfold; split; try lra; easy.
+apply R_second_countable.
+(* *)
+exists (bij_Q2N (0, 0)%Q).
+unfold topo_basis_R; rewrite bij_NQ2N; simpl; intros x Hx; lra.
 Qed.
 
 (* Lem 492 p. 70 *)

Lebesgue/measurable_Rbar.v

@@ -259,10 +259,10 @@ apply measurable_Rbar_R_eq_lt.
 Qed.
 *)
 
-Lemma gen_Rbar_topo_basis_empty : gen_Rbar_topo_basis emptyset.
+Lemma gen_Rbar_topo_basis_empty : exists n, empty (topo_basis_Rbar n).
 Proof.
 pose (n := bij_Q2N (0, 0)%Q).
-rewrite subset_ext with (B := topo_basis_Rbar (2 * n + 1)%nat); try easy.
+exists (2 * n + 1)%nat.
 unfold topo_basis_Rbar.
 destruct (Even_Odd_dec (2 * n + 1)%nat) as [Hn | Hn].
 destruct (Nat.Even_Odd_False _ Hn); exists n; easy.
@@ -272,20 +272,10 @@ Qed.
 Lemma measurable_Rbar_Borel_eq_topo_basis :
   measurable_Rbar_Borel = measurable gen_Rbar_topo_basis.
 Proof.
-apply measurable_Borel_gen_ext; intros B HB.
-(* *)
-induction HB as [n]; unfold topo_basis_Rbar.
-destruct (Even_Odd_dec n).
-destruct (Even_Odd_dec (Nat.div2 n)).
-apply open_Rbar_lt.
-apply open_Rbar_gt.
-apply open_Rbar_intoo.
-(* *)
-destruct (Rbar_second_countable_alt B HB) as [P HP].
-exists (fun n => inter (Prop_cst (P n)) (topo_basis_Rbar n)); split; try easy.
-subset_unfold; intros n; case (in_dec P n); intros Hn.
-rewrite subset_ext with (B := topo_basis_Rbar n); easy.
-rewrite subset_ext with (B := emptyset); try easy.
+unfold measurable_Rbar_Borel.
+rewrite (measurable_Borel_eq_topo_basis topo_basis_Rbar).
+f_equal; apply subset_ext_equiv; split; intros x Hx; induction Hx; easy.
+apply Rbar_second_countable.
 apply gen_Rbar_topo_basis_empty.
 Qed.