equal
deleted
inserted
replaced
215 where "field(r) == domain(r) \<union> range(r)" |
215 where "field(r) == domain(r) \<union> range(r)" |
216 |
216 |
217 definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close> |
217 definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close> |
218 where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>" |
218 where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>" |
219 |
219 |
220 definition function :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close> |
220 definition "function" :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close> |
221 where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')" |
221 where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')" |
222 |
222 |
223 definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close> |
223 definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close> |
224 where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}" |
224 where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}" |
225 |
225 |