equal
deleted
inserted
replaced
1871 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T" |
1871 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T" |
1872 by (force simp: pairwise_def) |
1872 by (force simp: pairwise_def) |
1873 |
1873 |
1874 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A" |
1874 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A" |
1875 by (auto simp: pairwise_def) |
1875 by (auto simp: pairwise_def) |
|
1876 |
|
1877 lemma pairwise_imageI: |
|
1878 "pairwise P (f ` A)" |
|
1879 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)" |
|
1880 using that by (auto intro: pairwiseI) |
1876 |
1881 |
1877 lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s" |
1882 lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s" |
1878 by (force simp: pairwise_def) |
1883 by (force simp: pairwise_def) |
1879 |
1884 |
1880 definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
1885 definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |