equal
deleted
inserted
replaced
240 where "f`a == \<Union>(f``{a})" |
240 where "f`a == \<Union>(f``{a})" |
241 |
241 |
242 definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
242 definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
243 where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}" |
243 where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}" |
244 |
244 |
245 abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr \<open>->\<close> 60) \<comment> \<open>function space\<close> |
245 abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr \<open>\<rightarrow>\<close> 60) \<comment> \<open>function space\<close> |
246 where "A -> B \<equiv> Pi(A, \<lambda>_. B)" |
246 where "A \<rightarrow> B \<equiv> Pi(A, \<lambda>_. B)" |
247 |
247 |
248 |
248 |
249 (* binder syntax *) |
249 (* binder syntax *) |
250 |
250 |
251 syntax |
251 syntax |
262 |
262 |
263 notation (ASCII) |
263 notation (ASCII) |
264 cart_prod (infixr \<open>*\<close> 80) and |
264 cart_prod (infixr \<open>*\<close> 80) and |
265 Int (infixl \<open>Int\<close> 70) and |
265 Int (infixl \<open>Int\<close> 70) and |
266 Un (infixl \<open>Un\<close> 65) and |
266 Un (infixl \<open>Un\<close> 65) and |
267 function_space (infixr \<open>\<rightarrow>\<close> 60) and |
267 function_space (infixr \<open>->\<close> 60) and |
268 Subset (infixl \<open><=\<close> 50) and |
268 Subset (infixl \<open><=\<close> 50) and |
269 mem (infixl \<open>:\<close> 50) and |
269 mem (infixl \<open>:\<close> 50) and |
270 not_mem (infixl \<open>~:\<close> 50) |
270 not_mem (infixl \<open>~:\<close> 50) |
271 |
271 |
272 syntax (ASCII) |
272 syntax (ASCII) |