Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1983P3

module

public import Mathlib.Data.Finset.Max
public import Mathlib.Data.Real.Basic
public import Mathlib.Data.Set.Card
public import Mathlib.Tactic.Choose

public section


/-!
# USA Mathematical Olympiad 1983, Problem 3

S₁, S₂, ..., Sₙ are subsets of the real line. Each Sᵢ is the union of two
closed intervals. Any three Sᵢ have a point in common. Show that there is a
point which belongs to at least half the Sᵢ.
-/

namespace Usa1983P3

theorem usa1983_p3 {n : ℕ} (hn : 0 < n) (S : Fin n → Set ℝ)
    (hS : ∀ i, ∃ a b c d : ℝ, a ≤ b ∧ b ≤ c ∧ c ≤ d ∧
      S i = Set.Icc a b ∪ Set.Icc c d)
    (h3 : ∀ i j k : Fin n, (S i ∩ S j ∩ S k).Nonempty) :
    ∃ x : ℝ, n ≤ 2 * {i : Fin n | x ∈ S i}.ncard := sorry

end Usa1983P3

File author(s): Kimi K3

This problem has a complete formalized solution.