Pigeonhole principle
Prove the pigeonhole principle; that is, if \(S\) is a finite set and \(T\) and \(U\) are subsets of \(S\) such that the number of elements of \(S\) is less than the sum of the number of elements of \(T\) and \(U\), then the intersection of \(T\) and \(U\) is non-empty.
To do this, complete the following Lean4 theory:
import Mathlib.Data.Finset.Card open Finset variable [DecidableEq α] variable {s t u : Finset α} set_option pp.fieldNotation false example (hts : t ⊆ s) (hus : u ⊆ s) (hstu : card s < card t + card u) : Finset.Nonempty (t ∩ u) := by sorry
1. Proof in natural language
By contradiction. For this, let's assume that \[ T ∩ U = ∅ \tag{1} \] and we have to prove that \[ \text{card}(T) + \text{card}(U) ≤ \text{card}(S) \tag{2} \]
The inequality (2) is proved by the following chain of relations: \begin{align} \text{card}(T) + \text{card}(U) &= \text{card}(T ∪ U) + \text{card}(T ∩ U) \newline &= \text{card}(T ∪ U) + 0 &&\text{[by (1)]} \newline &= \text{card}(T ∪ U) \newline &≤ \text{card}(S) &&\text{[because \(T ⊆ S\) and \(U ⊆ S\)]} \end{align}
2. Proofs with Lean4
import Mathlib.Data.Finset.Card open Finset variable [DecidableEq α] variable {s t u : Finset α} set_option pp.fieldNotation false -- Proof 1 -- ======= example (hts : t ⊆ s) (hus : u ⊆ s) (hstu : card s < card t + card u) : Finset.Nonempty (t ∩ u) := by contrapose! hstu -- hstu : ¬Finset.Nonempty (t ∩ u) -- ⊢ card t + card u ≤ card s have h1 : t ∩ u = ∅ := not_nonempty_iff_eq_empty.mp hstu have h2 : card (t ∩ u) = 0 := card_eq_zero.mpr h1 calc card t + card u = card (t ∪ u) + card (t ∩ u) := (card_union_add_card_inter t u).symm _ = card (t ∪ u) + 0 := congrArg (card (t ∪ u) + .) h2 _ = card (t ∪ u) := add_zero (card (t ∪ u)) _ ≤ card s := card_le_card (union_subset hts hus) -- Proof 2 -- ======= example (hts : t ⊆ s) (hus : u ⊆ s) (hstu : card s < card t + card u) : Finset.Nonempty (t ∩ u) := by contrapose! hstu -- hstu : ¬Finset.Nonempty (t ∩ u) -- ⊢ card t + card u ≤ card s calc card t + card u = card (t ∪ u) + card (t ∩ u) := (card_union_add_card_inter t u).symm _ = card (t ∪ u) + 0 := congrArg (card (t ∪ u) + .) (card_eq_zero.mpr (not_nonempty_iff_eq_empty.mp hstu)) _ = card (t ∪ u) := add_zero (card (t ∪ u)) _ ≤ card s := card_le_card (union_subset hts hus) -- Proof 3 -- ======= example (hts : t ⊆ s) (hus : u ⊆ s) (hstu : card s < card t + card u) : Finset.Nonempty (t ∩ u) := by contrapose! hstu -- hstu : ¬Finset.Nonempty (t ∩ u) -- ⊢ card t + card u ≤ card s calc card t + card u = card (t ∪ u) := by simp [← card_union_add_card_inter, not_nonempty_iff_eq_empty.1 hstu] _ ≤ card s := by gcongr; exact union_subset hts hus -- Proof 4 -- ======= example (hts : t ⊆ s) (hus : u ⊆ s) (hstu : card s < card t + card u) : Finset.Nonempty (t ∩ u) := inter_nonempty_of_card_lt_card_add_card hts hus hstu -- Used lemmas -- =========== -- variable (a : ℕ) -- #check (add_zero a : a + 0 = a) -- #check (card_eq_zero : card s = 0 ↔ s = ∅) -- #check (card_le_card : s ⊆ t → card s ≤ card t) -- #check (card_union_add_card_inter s t : card (s ∪ t) + card (s ∩ t) =card s + card t) -- #check (inter_nonempty_of_card_lt_card_add_card : t ⊆ s → u ⊆ s → card s < card t + card u → Finset.Nonempty (t ∩ u)) -- #check (not_nonempty_iff_eq_empty : ¬Finset.Nonempty s ↔ s = ∅) -- #check (union_subset : s ⊆ u → t ⊆ u → s ∪ t ⊆ u)
You can interact with the previous proofs at Lean 4 Web.