Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1978P5

module

public import Mathlib.AlgebraicTopology.SimplexCategory.Basic

public section


/-!
# USA Mathematical Olympiad 1978, Problem 5

There are 9 delegates at a conference, each speaking at most three languages.
Given any three delegates, at least 2 speak a common language.
Show that there are three delegates with a common language.
-/

namespace Usa1978P5

/-- Delegate `a` and delegate `b` speak a common language. -/
abbrev Share {L : Type*} (speaks : Fin 9 → Finset L) (a b : Fin 9) : Prop :=
  ∃ l : L, l ∈ speaks a ∧ l ∈ speaks b

theorem usa1978_p5 {L : Type*} (speaks : Fin 9 → Finset L)
    (hthree : ∀ d : Fin 9, (speaks d).card ≤ 3)
    (hpair : ∀ a b c : Fin 9, a ≠ b → a ≠ c → b ≠ c →
      Share speaks a b ∨ Share speaks b c ∨ Share speaks a c) :
    ∃ a b c : Fin 9, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
      ∃ l : L, l ∈ speaks a ∧ l ∈ speaks b ∧ l ∈ speaks c := sorry

end Usa1978P5

File author(s): Kimi K3

This problem has a complete formalized solution.