Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2011P6

module

public import Mathlib.Algebra.Order.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star

public section


/-!
# USA Mathematical Olympiad 2011, Problem 6

Let A be a set with |A| = 225, meaning that A has 225 elements. Suppose further
that there are eleven subsets A₁, A₂, ..., A₁₁ of A such that |Aᵢ| = 45 for
1 ≤ i ≤ 11 and |Aᵢ ∩ Aⱼ| = 9 for 1 ≤ i < j ≤ 11. Prove that
|A₁ ∪ A₂ ∪ ··· ∪ A₁₁| ≥ 165, and give an example for which equality holds.
-/

namespace Usa2011P6

theorem usa2011_p6 {α : Type*} [DecidableEq α] (A : Finset α) (As : Fin 11 → Finset α)
    (hA : A.card = 225) (hsub : ∀ i, As i ⊆ A)
    (hcard : ∀ i, (As i).card = 45)
    (hinter : ∀ i j, i ≠ j → (As i ∩ As j).card = 9) :
    165 ≤ (Finset.univ.biUnion As).card := sorry

theorem usa2011_p6_sharp :
    ∃ A : Finset (Finset (Fin 11) ⊕ Fin 60),
      ∃ As : Fin 11 → Finset (Finset (Fin 11) ⊕ Fin 60),
        A.card = 225 ∧ (∀ i, As i ⊆ A) ∧ (∀ i, (As i).card = 45) ∧
        (∀ i j, i ≠ j → (As i ∩ As j).card = 9) ∧
        (Finset.univ.biUnion As).card = 165 := sorry

end Usa2011P6

File author(s): Kimi K3

This problem has a complete formalized solution.