WIP: measurable_Borel_prod_eq.

Lebesgue/measurable.v

@@ -259,8 +259,11 @@ Context {E1 E2 : Type}. (* Universes. *)
 Variable genE1 : (E1 -> Prop) -> Prop. (* Generator. *)
 Variable genE2 : (E2 -> Prop) -> Prop. (* Generator. *)
 
+Definition Prod_measurable : (E1 * E2 -> Prop) -> Prop :=
+  Prod (measurable genE1) (measurable genE2).
+
 Definition measurable_Prod : (E1 * E2 -> Prop) -> Prop :=
-  measurable (Prod_Sigma_algebra genE1 genE2).
+  measurable Prod_measurable.
 
 End Cartesian_product_def.
 
@@ -379,8 +382,24 @@ Let genExF := Gen_Prod (@open E) (@open F).
 (* From Lem 701 p. 135,136 (RR-9386-v3) (with m := 2 and Y_i := X_i). *)
 Lemma measurable_Borel_prod_eq : measurable_Borel = measurable genExF.
 Proof.
-unfold measurable_Borel, genExF.
-apply measurable_gen_ext; intros A HA.
+apply measurable_Borel_alt_gen.
+(* *)
+
+
+
+
+
+
+
+
+
 Admitted.
 
+(* From Lem 701 p. 135,136 (RR-9386-v3) (with m := 2 and Y_i := X_i). *)
+Lemma measurable_Borel_prod_eq_alt :
+  measurable_Borel = measurable_Prod (@open E) (@open F).
+Proof.
+rewrite measurable_Borel_prod_eq, measurable_Prod_eq; easy.
+Qed.
+
 End Borel_Cartesian_product.