rebase

theories/kernel.v

@@ -41,18 +41,6 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 Local Open Scope ereal_scope.
 
-(* PR in progress *)
-Lemma emeasurable_itv (R : realType) (i : interval (\bar R)) :
-  measurable ([set` i]%classic : set \bar R).
-Proof.
-rewrite -[X in measurable X]setCK; apply: measurableC.
-rewrite set_interval.setCitv /=; apply: measurableU => [|].
-- move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE//.
-  exact: emeasurable_itv_ninfty_bnd.
-- move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE//.
-  exact: emeasurable_itv_bnd_pinfty.
-Qed.
-
 Section sfinite_fubini.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variables (m1 : {sfinite_measure set X -> \bar R}).