Add Image/Preimage.

WIP: add facts about Image/Preimage.

Lebesgue/measurable.v

@@ -171,7 +171,7 @@ Qed.
 End measurable_Facts.
 
 
-Section measurable_gen_Facts.
+Section measurable_gen_Facts1.
 
 (** Properties of the "generation" of measurability. *)
 
@@ -237,7 +237,70 @@ Proof.
 apply Sigma_algebra_gen_add_eq.
 Qed.
 
-End measurable_gen_Facts.
+End measurable_gen_Facts1.
+
+
+Section measurable_gen_Image_Def.
+
+Context {E F : Type}. (* Universes. *)
+
+Variable f : E -> F.
+Variable PE : (E -> Prop) -> Prop. (* Subset system. *)
+Variable PF : (F -> Prop) -> Prop. (* Subset system. *)
+
+Definition Image : (F -> Prop) -> Prop := fun B => PE (preimage f B).
+
+Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
+
+End measurable_gen_Image_Def.
+
+
+Section measurable_gen_Facts2.
+
+Context {E F : Type}. (* Universes. *)
+Variable genE : (E -> Prop) -> Prop. (* Generator. *)
+Variable genF : (F -> Prop) -> Prop. (* Generator. *)
+
+Variable f : E -> F.
+
+Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE)).
+Proof.
+apply Sigma_algebra_equiv; repeat split.
+apply measurable_empty.
+intros B HB; apply measurable_compl; easy.
+intros B HB; apply measurable_union_seq; easy.
+Qed.
+
+Lemma is_Sigma_algebra_Preimage :
+  is_Sigma_algebra (Preimage f (measurable genF)).
+Proof.
+apply Sigma_algebra_equiv; repeat split.
+(* *)
+exists emptyset; split.
+apply measurable_empty.
+symmetry; apply preimage_emptyset.
+(* *)
+intros A [B HB]; exists (compl B); split.
+apply measurable_compl; easy.
+rewrite preimage_compl; f_equal; easy.
+(* *)
+intros A HA.
+unfold image in HA.
+destruct (ClassicalChoice.choice
+    (fun n Bn => measurable genF Bn /\ A n = preimage f Bn) HA) as [B HB].
+exists (union_seq B); split.
+apply measurable_union_seq; intros n; apply HB.
+rewrite preimage_union_seq; f_equal.
+apply subset_seq_ext.
+intros n; rewrite (proj2 (HB n)); easy.
+Qed.
+
+Lemma measurable_gen_Preimage :
+  measurable (Preimage f genF) = Preimage f (measurable genF).
+Proof.
+Admitted.
+
+End measurable_gen_Facts2.
 
 
 Section measurable_correct.