Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2007P3

module

public import Mathlib.Data.Finset.Card
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2007, Problem 3

Let S be a set containing n² + n − 1 elements. Suppose that the n-element
subsets of S are partitioned into two classes. Prove that there are at least
n pairwise disjoint sets in the same class.
-/

namespace Usa2007P3

theorem usa2007_p3 (n : ℕ) (hn : 0 < n) {α : Type*} [DecidableEq α] (S : Finset α)
    (hS : S.card = n ^ 2 + n - 1) (col : Finset α → Bool) :
    ∃ F : Finset (Finset α), n ≤ F.card ∧ (∀ A ∈ F, A ⊆ S ∧ A.card = n) ∧
      (F : Set (Finset α)).PairwiseDisjoint id ∧ ∃ b : Bool, ∀ A ∈ F, col A = b := sorry

end Usa2007P3

File author(s): Kimi K3

This problem has a complete formalized solution.