author Manuel Eberl Wed, 13 May 2020 13:00:03 +0200 changeset 72063 5656ec95493c parent 72062 dca11678c495 child 72064 0bbe0866b7e6
generalised pigeonhole principle in HOL-Library.FuncSet
--- a/src/HOL/Library/FuncSet.thy	Wed May 13 12:55:33 2020 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed May 13 13:00:03 2020 +0200
@@ -686,4 +686,35 @@
by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
qed

+subsection \<open>The pigeonhole principle\<close>
+
+text \<open>
+  An alternative formulation of this is that for a function mapping a finite set \<open>A\<close> of
+  cardinality \<open>m\<close> to a finite set \<open>B\<close> of cardinality \<open>n\<close>, there exists an element \<open>y \<in> B\<close> that
+  is hit at least $\lceil \frac{m}{n}\rceil$ times. However, since we do not have real numbers
+  or rounding yet, we state it in the following equivalent form:
+\<close>
+lemma pigeonhole_card:
+  assumes "f \<in> A \<rightarrow> B" "finite A" "finite B" "B \<noteq> {}"
+  shows   "\<exists>y\<in>B. card (f - {y} \<inter> A) * card B \<ge> card A"
+proof -
+  from assms have "card B > 0"
+    by auto
+  define M where "M = Max ((\<lambda>y. card (f - {y} \<inter> A))  B)"
+  have "A = (\<Union>y\<in>B. f - {y} \<inter> A)"
+    using assms by auto
+  also have "card \<dots> = (\<Sum>i\<in>B. card (f - {i} \<inter> A))"
+    using assms by (subst card_UN_disjoint) auto
+  also have "\<dots> \<le> (\<Sum>i\<in>B. M)"
+    unfolding M_def using assms by (intro sum_mono Max.coboundedI) auto
+  also have "\<dots> = card B * M"
+    by simp
+  finally have "M * card B \<ge> card A"
+  moreover have "M \<in> (\<lambda>y. card (f - {y} \<inter> A))  B"
end`