# Theory Binomial_Lemmas

section ‹Lemmas involving the binomial coefficient›
text ‹In this section, we prove lemmas that use the term for the binomial coefficient @{term choose}.›
theory Binomial_Lemmas
imports Main
begin
lemma choose_mono:
assumes "x ≤ y"
shows "x choose n ≤ y choose n"
proof -
have "finite {0..<y}" by blast
with finite_Pow_iff[of "{0..<y}"] have finiteness: "finite {K ∈ Pow {0..<y}. card K = n}" by simp
from assms have "Pow {0..<x} ⊆ Pow {0..<y}" by force
then have "{K ∈ Pow {0..<x}. card K = n} ⊆ {K ∈ Pow {0..<y}. card K = n}" by blast
from card_mono[OF finiteness this] show ?thesis unfolding binomial_def .
qed
lemma choose_row_sum_set:
assumes "finite (⋃F)"
shows "card {S. S ⊆ ⋃F ∧ card S ≤ k} = (∑i≤k. card (⋃ F) choose i)"
proof (induction k)
case 0
from rev_finite_subset[OF assms] have "S ⊆ ⋃F ∧ card S ≤ 0 ⟷ S = {}" for S by fastforce
then show ?case by simp
next
case (Suc k)
let ?FS = "{S. S ⊆ ⋃ F ∧ card S ≤ Suc k}"
and ?F_Asm = "{S. S ⊆ ⋃ F ∧ card S ≤ k}"
and ?F_Step = "{S. S ⊆ ⋃ F ∧ card S = Suc k}"
from finite_Pow_iff[of "⋃F"] assms have finite_Pow_Un_F: "finite (Pow (⋃ F))" ..
have "?F_Asm ⊆ Pow (⋃ F)" and "?F_Step ⊆ Pow (⋃ F)" by fast+
with rev_finite_subset[OF finite_Pow_Un_F] have finite_F_Asm: "finite ?F_Asm" and finite_F_Step: "finite ?F_Step" by presburger+
have F_Un: "?FS = ?F_Asm ∪ ?F_Step" and F_disjoint: "?F_Asm ∩ ?F_Step = {}" by fastforce+
from card_Un_disjoint[OF finite_F_Asm finite_F_Step F_disjoint] F_Un have "card ?FS = card ?F_Asm + card ?F_Step" by argo
also from Suc have "... = (∑i≤k. card (⋃ F) choose i) + card ?F_Step" by argo
also from n_subsets[OF assms, of "Suc k"] have "... = (∑i≤Suc k. card (⋃ F) choose i)" by force
finally show ?case by blast
qed
end