Merge pull request #363 from math-comp/remove_measurableT_duplicate

Remove measurableT which is already defined
math-comp · Apr 1, 2021 · 4098cb9 · 4098cb9
2 parents 89df81c + 4bb0b17
commit 4098cb9
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.