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 chapter28.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

theorem chapter28.handshaking {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} [DecidableRel G.Adj] : ∑ v : α, G.degree v = 2 * G.edgeFinset.card