src/ZF/ZF.thy
 changeset 65386 e3fb3036a00e parent 63901 4ce989e962e0 child 65464 f3cd78ba687c
equal inserted replaced
65385:23f36ab9042b 65386:e3fb3036a00e
`   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 `