generalizing inj_on_Int
authorbulwahn
Wed Feb 22 08:05:28 2012 +0100 (2012-02-22)
changeset 46586abbec6fa25c8
parent 46585 f462e49eaf11
child 46587 d3bcc356cc60
generalizing inj_on_Int
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 22 08:01:41 2012 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Feb 22 08:05:28 2012 +0100
     1.3 @@ -166,7 +166,7 @@
     1.4  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
     1.5  by (simp add: inj_on_def)
     1.6  
     1.7 -lemma inj_on_Int: "\<lbrakk>inj_on f A; inj_on f B\<rbrakk> \<Longrightarrow> inj_on f (A \<inter> B)"
     1.8 +lemma inj_on_Int: "inj_on f A \<or> inj_on f B \<Longrightarrow> inj_on f (A \<inter> B)"
     1.9  unfolding inj_on_def by blast
    1.10  
    1.11  lemma inj_on_INTER: