Using new Inductive image.

Lebesgue/measurable_fun-new.v

@@ -29,38 +29,6 @@ Require Import Subset Subset_dec Subset_system_base measurable.
 Open Scope nat_scope.
 
 
-Section compl1.
-
-Context {E F : Type}. (* Universes. *)
-
-Variable f : E -> F. (* Function. *)
-Variable AE : E -> Prop. (* Subset. *)
-Variable AF : F -> Prop. (* Subset. *)
-
-Inductive image : F -> Prop := Im : forall x, AE x -> image (f x).
-
-Definition preimage : E -> Prop := fun x => AF (f x).
-
-End compl1.
-
-
-Section compl2.
-
-Context {E F : Type}. (* Universes. *)
-
-Variable f : E -> F. (* Function. *)
-Variable PE : (E -> Prop) -> Prop. (* Subset system. *)
-Variable PF : (F -> Prop) -> Prop. (* Subset system. *)
-
-(* From Lemma 524 p. 93 (v2) *)
-Definition Image : (F -> Prop) -> Prop := fun AF => PE (preimage f AF).
-
-(* From Lemma 523 p. 93 (v2) *)
-Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
-
-End compl2.
-
-
 Section Measurable_fun_Def.
 
 Context {E F : Type}.
@@ -74,19 +42,15 @@ Definition measurable_fun : (E -> F) -> Prop :=
 Lemma measurable_fun_ext :
   forall f g, same_fun f g -> measurable_fun f -> measurable_fun g.
 Proof.
-intros f g H Hf AE HAE; induction HAE as [AF HAF].
-rewrite <- (preimage_ext_fun f); try easy.
-
-
-intros f g H Hf A [B HB]; rewrite (proj2 HB); apply Hf.
-exists B; split; try easy.
-apply preimage_ext_fun; easy.
+intros f g H Hf AE [AF HAF].
+rewrite <- (preimage_ext_fun f); try easy; apply Hf; easy.
 Qed.
 
 (* Lemma 526 p. 93 (v2) *)
 Lemma measurable_fun_cst : forall y, measurable_fun (fun _ => y).
 Proof.
-intros y A [B HB]; destruct (in_dec B y). ; apply measurable_Prop.
+intros y AE [AF HAF]; destruct (in_dec AF y) as [Hy | Hy].
+; apply measurable_Prop.
 Qed.
 
 (* Lemma 528 p. 94 *)