src/HOL/Set.thy
changeset 67051 e7e54a0b9197
parent 66802 627511c13164
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Set.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Set.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -1874,6 +1874,11 @@
     1.4  lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
     1.5    by (auto simp: pairwise_def)
     1.6  
     1.7 +lemma pairwise_imageI:
     1.8 +  "pairwise P (f ` A)"
     1.9 +  if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)"
    1.10 +  using that by (auto intro: pairwiseI)
    1.11 +
    1.12  lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
    1.13    by (force simp: pairwise_def)
    1.14