Pigeon-hole and double counting

TODO

• statement
• 1. Numbers
  • Claim
  • Claim
• 2. Sequences
  • Claim
    • proof
• 3. Sums
  • Claim
• Double Counting
• 4. Numbers again
• 5. Graphs
  • Theorem
    • proof
  • Claim
• 6. Sperner's Lemma
  • proof
  • Proof of Brouwer's fixed point theorem (for $n = 2$)

theorem pigeon_hole_principle (n : ℕ) (r : ℕ) (h : r < n) (object_to_boxes : Fin n → Fin r) : ∃ (box : Fin r) (object₁ : Fin n) (object₂ : Fin n), object₁ ≠ object₂ ∧ object_to_boxes object₁ = box ∧ object_to_boxes object₂ = box