diff -r ee8edbcbb4ad -r af0e964aad7b src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Tue May 17 08:40:24 2016 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Tue May 17 17:05:35 2016 +0200
@@ -111,6 +111,9 @@
 lemma (in prob_space) emeasure_le_1: "emeasure M S \<le> 1"
   unfolding ennreal_1[symmetric] emeasure_eq_measure by (subst ennreal_le_iff) auto
 
+lemma (in prob_space) emeasure_ge_1_iff: "emeasure M A \<ge> 1 \<longleftrightarrow> emeasure M A = 1"
+  by (rule iffI, intro antisym emeasure_le_1) simp_all
+
 lemma (in prob_space) AE_iff_emeasure_eq_1:
   assumes [measurable]: "Measurable.pred M P"
   shows "(AE x in M. P x) \<longleftrightarrow> emeasure M {x\<in>space M. P x} = 1"
@@ -125,6 +128,9 @@
 lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1"
   using emeasure_space[of M X] by (simp add: emeasure_space_1)
 
+lemma (in prob_space) measure_ge_1_iff: "measure M A \<ge> 1 \<longleftrightarrow> measure M A = 1"
+  by (auto intro!: antisym)  
+
 lemma (in prob_space) AE_I_eq_1:
   assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M"
   shows "AE x in M. P x"