WIP: proof of measurable_gen_Preimage.

Lebesgue/measurable.v

@@ -255,6 +255,43 @@ Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
 End measurable_gen_Image_Def.
 
 
+Section measurable_gen_Image_Facts.
+
+Context {E F : Type}. (* Universes. *)
+
+Variable f : E -> F.
+Variable PE1 PE2 : (E -> Prop) -> Prop. (* Subset systems. *)
+Variable PF1 PF2 : (F -> Prop) -> Prop. (* Subset systems. *)
+
+Lemma Image_monot : Incl PE1 PE2 -> Incl (Image f PE1) (Image f PE2).
+Proof.
+intros H B HB; apply H; easy.
+Qed.
+
+Lemma Preimage_monot : Incl PF1 PF2 -> Incl (Preimage f PF1) (Preimage f PF2).
+Proof.
+apply image_monot.
+Qed.
+
+Lemma Preimage_of_Image : Incl (Preimage f (Image f PE1)) PE1.
+Proof.
+intros A [B [HB1 HB2]]; rewrite HB2; easy.
+Qed.
+
+Lemma Image_of_Preimage : Incl PF1 (Image f (Preimage f PF1)).
+Proof.
+intros B HB; exists B; easy.
+Qed.
+
+Lemma toto : Incl PF1 (Image f PE1) -> Incl (Preimage f PF1) PE1.
+Proof.
+intros; apply Incl_trans with (Preimage f (Image f PE1)).
+(*apply Preimage_monot.*)
+Admitted.
+
+End measurable_gen_Image_Facts.
+
+
 Section measurable_gen_Facts2.
 
 Context {E F : Type}. (* Universes. *)
@@ -298,6 +335,16 @@ Qed.
 Lemma measurable_gen_Preimage :
   measurable (Preimage f genF) = Preimage f (measurable genF).
 Proof.
+apply Ext_equiv; split.
+(* *)
+rewrite <- is_Sigma_algebra_Preimage.
+apply measurable_gen_monot, Preimage_monot, measurable_gen.
+(* *)
+
+
+
+
+
 Admitted.
 
 End measurable_gen_Facts2.