diff -r c6e9c7d140ff -r 2d79288b042c src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Jun 22 16:31:29 2017 +0100
@@ -1379,6 +1379,13 @@
   shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
   using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
 
+lemma borel_measurable_uminus_eq [simp]:
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
+  shows "(\<lambda>x. - f x) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
+proof
+  assume ?l from borel_measurable_uminus[OF this] show ?r by simp
+qed auto
+
 lemma affine_borel_measurable_vector:
   fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
   assumes "f \<in> borel_measurable M"