62 |
62 |
63 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where |
63 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where |
64 "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" |
64 "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" |
65 |
65 |
66 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV" |
66 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV" |
|
67 |
|
68 lemma disjoint_family_elem_disjnt: |
|
69 assumes "infinite A" "finite C" |
|
70 and df: "disjoint_family_on B A" |
|
71 obtains x where "x \<in> A" "disjnt C (B x)" |
|
72 proof - |
|
73 have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x" |
|
74 proof - |
|
75 obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x" |
|
76 using * by metis |
|
77 with df have "inj_on g A" |
|
78 by (fastforce simp add: inj_on_def disjoint_family_on_def) |
|
79 then have "infinite (g ` A)" |
|
80 using \<open>infinite A\<close> finite_image_iff by blast |
|
81 then show False |
|
82 by (meson \<open>finite C\<close> finite_subset g image_subset_iff) |
|
83 qed |
|
84 then show ?thesis |
|
85 by (force simp: disjnt_iff intro: that) |
|
86 qed |
67 |
87 |
68 lemma disjoint_family_onD: |
88 lemma disjoint_family_onD: |
69 "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}" |
89 "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}" |
70 by (auto simp: disjoint_family_on_def) |
90 by (auto simp: disjoint_family_on_def) |
71 |
91 |