Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1986P2

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Finset.Powerset
public import Mathlib.Data.Real.Basic
public import Mathlib.Tactic.Choose
public import Mathlib.Tactic.NormNum

public section


/-!
# USA Mathematical Olympiad 1986, Problem 2

Five professors attended a lecture. Each fell asleep just twice. For each pair
there was a moment when both were asleep. Show that there was a moment when
three of them were asleep.
-/

namespace Usa1986P2

/-- Each professor `p : Fin 5` takes two naps, and nap `k : Fin 2` of professor
`p` is the closed interval `[s p k, e p k]`. Professor `p` is asleep at time
`t` if `t` belongs to one of these two nap intervals. -/
def Asleep (s e : Fin 5 → Fin 2 → ℝ) (p : Fin 5) (t : ℝ) : Prop :=
  ∃ k : Fin 2, s p k ≤ t ∧ t ≤ e p k

theorem usa1986_p2 (s e : Fin 5 → Fin 2 → ℝ)
    (hsleep : ∀ p q : Fin 5, p ≠ q → ∃ t, Asleep s e p t ∧ Asleep s e q t) :
    ∃ t : ℝ, ∃ p q r : Fin 5, p ≠ q ∧ p ≠ r ∧ q ≠ r ∧
      Asleep s e p t ∧ Asleep s e q t ∧ Asleep s e r t := sorry

end Usa1986P2

File author(s): Kimi K3

This problem has a complete formalized solution.