From 387dba4a98c5802f5154d8219d344798b5d44d9e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 15 Mar 2023 12:46:02 +0900 Subject: [PATCH] rebase --- theories/kernel.v | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/theories/kernel.v b/theories/kernel.v index 2161f1762c..b644b2345b 100644 --- a/theories/kernel.v +++ b/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}).