Remove measurableT which is already defined

math-comp · Apr 1, 2021 · 4bb0b17 · 4bb0b17
1 parent a21bb29
commit 4bb0b17
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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.