src/ZF/OrdQuant.thy
changeset 13149 773657d466cb
parent 13118 336b0bcbd27c
child 13162 660a71e712af
equal deleted inserted replaced
13148:fe118a977a6d 13149:773657d466cb
    82 
    82 
    83 lemma function_lam: "function (lam x:A. b(x))"
    83 lemma function_lam: "function (lam x:A. b(x))"
    84 by (simp add: function_def lam_def) 
    84 by (simp add: function_def lam_def) 
    85 
    85 
    86 lemma relation_lam: "relation (lam x:A. b(x))"  
    86 lemma relation_lam: "relation (lam x:A. b(x))"  
    87 by (simp add: relation_def lam_def, blast) 
    87 by (simp add: relation_def lam_def) 
    88 
    88 
    89 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
    89 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
    90 by (simp add: restrict_def) 
    90 by (simp add: restrict_def) 
    91 
    91 
    92 (** These mostly belong to theory Ordinal **)
    92 (** These mostly belong to theory Ordinal **)