WIP.

Lebesgue/measurable.v

@@ -521,6 +521,11 @@ 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 -> 
+*)
+
 End Borel_subsets.