# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1692738831 -3600
# Node ID f675e2a316826fbb6476f4faa1d5dd77acf3e2b8
# Parent  9c547cdf837974e3e14cb35fe8638a0fc4696a5c
A subtle fix involving the "measurable" attribute

diff -r 9c547cdf8379 -r f675e2a31682 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Mon Aug 21 18:38:41 2023 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Tue Aug 22 22:13:51 2023 +0100
@@ -1894,8 +1894,16 @@
   then show ?thesis unfolding A_def by simp
 qed
 
+text \<open>Logically equivalent to those with the opposite orientation, still these are needed\<close>
+lemma measurable_inequality_set_flipped:
+  fixes f g::"_ \<Rightarrow> 'a::{second_countable_topology, linorder_topology}"
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  shows "{x \<in> space M. f x \<ge> g x} \<in> sets M"
+        "{x \<in> space M. f x > g x} \<in> sets M"
+  by auto
+
 lemmas measurable_inequality_set [measurable] =
-  borel_measurable_le borel_measurable_less borel_measurable_le borel_measurable_less
+  borel_measurable_le borel_measurable_less measurable_inequality_set_flipped
 
 proposition measurable_limit [measurable]:
   fixes f::"nat \<Rightarrow> 'a \<Rightarrow> 'b::first_countable_topology"