infix syntax for measurable set
authorhoelzl
Wed, 25 Nov 2015 22:44:02 +0100
changeset 61847 9e38cde3d672
parent 61846 2c79790d270d
child 61849 f8741f200f91
infix syntax for measurable set
src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 25 22:44:02 2015 +0100
@@ -1700,7 +1700,7 @@
 
 subsubsection \<open>Measurable functions\<close>
 
-definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
   "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 
 lemma measurableI: