Migration of measurable_fun_compose, measurable_fun_swap_var, and

measurable_fun_swap.

Lebesgue/measurable_fun-new.v

@@ -22,7 +22,7 @@ COPYING file for more details.
 
  Some proof paths may differ. *)
 
-(*From Coquelicot Require Import Coquelicot.*)
+From Coquelicot Require Import Coquelicot.
 
 Require Import Subset Subset_dec Subset_seq.
 Require Import Subset_system_base Subset_system measurable.
@@ -101,7 +101,7 @@ Qed.
 End Measurable_fun_gen_ext.
 
 
-Section Measurable_fun_composition.
+Section Measurable_fun_Facts1.
 
 Context {E1 E2 E3 : Type}.
 
@@ -110,27 +110,21 @@ Variable genE2 : (E2 -> Prop) -> Prop.
 Variable genE3 : (E3 -> Prop) -> Prop.
 
 (* Lemma 530 p. 94 *)
-Lemma measurable_fun_composition :
+Lemma measurable_fun_compose :
   forall (f12 : E1 -> E2) (f23 : E2 -> E3),
     measurable_fun genE1 genE2 f12 ->
     measurable_fun genE2 genE3 f23 ->
-    measurable_fun genE1 genE3 (fun x1 => f23 (f12 x1)).
+    measurable_fun genE1 genE3 (compose f23 f12).
 Proof.
-intros f12 f23 H12 H23. unfold measurable_fun in *.
-apply Incl_trans with (Preimage f12 (measurable genE2)).
-apply H23.
-
-_ [A3 HA3].
-apply H12.
-apply H23.
- with (A2 := fun x1 => A2 (f23 x2)).
-now apply H2.
-Qed.
+intros f12 f23 H12 H23; unfold measurable_fun.
+rewrite Preimage_compose.
+eapply Incl_trans; [apply Preimage_monot, H23 | apply H12].
+Admitted.
 
-End Measurable_fun_composition.
+End Measurable_fun_Facts1.
 
 
-Section Measurable_fun_swap.
+Section Measurable_fun_Facts2.
 
 Context {E1 E2 F : Type}.
 
@@ -138,45 +132,41 @@ Context {genE1 : (E1 -> Prop) -> Prop}.
 Context {genE2 : (E2 -> Prop) -> Prop}.
 Context {genF : (F -> Prop) -> Prop}.
 
-Let genE1xE2 := Gen_Product genE1 genE2.
-Let genE2xE1 := Gen_Product genE2 genE1.
+Let genE1xE2 := Gen_Prod genE1 genE2.
+Let genE2xE1 := Gen_Prod genE2 genE1.
 
 Let swap_var := swap (fun x : E1 * E2 => x).
 
-Lemma measurable_fun_swap_var :
-  measurable_fun genE2xE1 genE1xE2 swap_var.
+Lemma measurable_fun_swap_var : measurable_fun genE2xE1 genE1xE2 swap_var.
 Proof.
-intros A HA; apply measurable_swap; easy.
+intros A21 [A12 HA12]; apply measurable_swap; easy.
 Qed.
 
 Lemma measurable_fun_swap :
   forall f, measurable_fun genE1xE2 genF f -> measurable_fun genE2xE1 genF (swap f).
 Proof.
 intros f Hf.
-apply measurable_fun_composition with (2:= Hf).
+apply measurable_fun_compose with (2 := Hf).
 apply measurable_fun_swap_var.
 Qed.
 
-End Measurable_fun_swap.
+End Measurable_fun_Facts2.
 
 
-Section Measurable_fun_continuous.
+Section Measurable_fun_Facts3.
 
 Context {E F : UniformSpace}.
 
-(* Lemma 529 p. 94 *)
+(* Lemma 529 p. 94 (v2) *)
 Lemma measurable_fun_continuous :
-  forall (f : E -> F),
-    (forall x, continuous f x) ->
-    measurable_fun open open f.
+  forall (f : E -> F), (forall x, continuous f x) -> measurable_fun open open f.
 Proof.
-intros f H.
-apply measurable_fun_gen.
-intros A HA.
-apply measurable_gen.
+intros f Hf; apply measurable_fun_equiv.
+intros A HA; apply measurable_gen.
+
 intros x Hx.
-apply H.
+apply Hf.
 now apply HA.
 Qed.
 
-End Measurable_fun_continuous.
+End Measurable_fun_Facts3.