WIP: proof of measurable_Rbar_Borel_correct.

Lebesgue/measurable_Rbar.v

@@ -158,7 +158,6 @@ Qed.
 Lemma measurable_Rbar_Borel_correct :
   measurable_Rbar_Borel = measurable_Borel_Rbar.
 Proof.
-(*
 apply Ext_equiv; split.
 (* *)
 rewrite measurable_Rbar_Borel_eq; unfold measurable_Borel_Rbar, measurable_Borel.
@@ -166,7 +165,7 @@ intros B HB.
 induction HB as [A HA | A HA | A HA | A HA]; rewrite measurable_R_eq_Borel in HA.
 (* . *)
 induction HA as [A HA | | A HA1 HA2 | A HA1 HA2].
-rewrite <- Rbar_subset_open_correct; apply measurable_gen; apply RbSO_bounded; easy.
+rewrite <- Rbar_subset_open_correct; apply measurable_gen; apply RbSO_woinf; easy.
 admit. (* rewrite up_id_empty. does not work! R vs R_UniformSpace... *)
 rewrite up_id_compl; apply measurable_compl.
 admit.
@@ -184,22 +183,20 @@ rewrite <- Rbar_subset_open_correct.
 intros A HA; induction HA as [A HA | B HB].
 (* . *)
 apply measurable_Rbar_Borel_R_open; easy.
-induction HB as [A a HA | | ].
 (* . *)
+induction HB as [A B HA HB | A a b HA].
+(* .. *)
 apply measurable_Rbar_Borel_union.
 apply measurable_Rbar_Borel_R_open; easy.
-apply measurable_Rbar_Borel_lt.
-(* . *)
-apply measurable_Rbar_Borel_union.
+induction HB as [b Hb | a Ha].
 apply measurable_Rbar_Borel_gt.
-apply measurable_Rbar_Borel_R_open; easy.
-(* . *)
+apply measurable_Rbar_Borel_lt.
+(* .. *)
 apply measurable_Rbar_Borel_union.
 apply measurable_Rbar_Borel_union.
-apply measurable_Rbar_Borel_gt.
 apply measurable_Rbar_Borel_R_open; easy.
+apply measurable_Rbar_Borel_gt.
 apply measurable_Rbar_Borel_lt.
-*)
 Admitted.
 
 End measurable_Rbar_Borel_Facts.