From 4bb0b17cb5e02f061f6c227cea2f3fcc76621d2f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 1 Apr 2021 09:35:20 +0200 Subject: [PATCH] Remove measurableT which is already defined --- theories/measure.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index cc5010c2a..7fd613501 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -209,9 +209,6 @@ Proof. by move=> mA; rewrite -setTD; apply measurableD => //; exact: measurableT. Qed. -Lemma measurableT : measurable (setT : set T). -Proof. by rewrite -setC0; apply measurableC; exact: measurable0. Qed. - Lemma measurable_bigcap (F : (set T)^nat) : (forall i, measurable (F i)) -> measurable (\bigcap_i (F i)). Proof.