rm dup emeasurable_funM (math-comp#924)

IshiguroYoshihiro · Sep 7, 2023 · f8adedd · f8adedd
1 parent 4eeb577
commit f8adedd
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -58,6 +58,8 @@
 - in `measure.v`:
   + instances `ae_filter_algebraOfSetsType`, `ae_filter_measurableType`,
   `ae_properfilter_measurableType`
+- in `lebesgue_integral.v`
+  + lemma `emeasurable_funN` (already in `lebesgue_measure.v`)
 
 ### Infrastructure
 

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -1591,12 +1591,6 @@ Unshelve. all: by end_near. Qed.
 
 End semi_linearity.
 
-Lemma emeasurable_funN d (T : measurableType d) (R : realType) D (f : T -> \bar R) :
-  measurable D -> measurable_fun D f -> measurable_fun D (fun x => - f x)%E.
-Proof.
-by move=> mD mf; apply: measurable_funT_comp => //; exact: emeasurable_fun_minus.
-Qed.
-
 Section approximation_sfun.
 Context d (T : measurableType d) (R : realType) (f : T -> \bar R).
 Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f).