-
Notifications
You must be signed in to change notification settings - Fork 8
/
Usa2024P2.lean
42 lines (32 loc) · 1.21 KB
/
Usa2024P2.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
/-
Copyright (c) 2024 The Compfiles Contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors:
-/
import Mathlib.Data.Set.Card
import Mathlib.Tactic
import ProblemExtraction
problem_file { tags := [.Combinatorics] }
/-!
# USA Mathematical Olympiad 2024, Problem 2
Let S₁, S₂, ..., Sₙ be finite sets of integers whose intersection
is not empty. For each non-empty T ⊆ {S₁, S₂, ..., Sₙ}, the size of
the intersection of the sets in T is a multiple of the number of
sets in T. What is the least possible number of elements that are in
at least 50 sets?
-/
namespace Usa2024P2
determine solution : ℕ := sorry
structure Good (S : Fin 100 → Set ℤ) : Prop where
finite : ∀ i, (S i).Finite
nonempty_inter : ⋂ i, S i ≠ ∅
card : ∀ T : Finset (Fin 100), T.Nonempty →
∃ k : ℕ, (⋂ i ∈ T, S i).ncard * k = T.card
-- z is in at least k of the sets S.
abbrev InAtLeastKSubsets (S : Fin 100 → Set ℤ) (k : ℕ) (z : ℤ) : Prop :=
k ≤ {i : Fin 100 | z ∈ S i }.ncard
problem usa2024_p2 (n : ℕ) :
IsLeast
{ k | ∃ S, Good S ∧
k = {z : ℤ | InAtLeastKSubsets S k z }.ncard } solution :=
by sorry