Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1988P3

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Data.Finset.Powerset
public import Mathlib.Order.Interval.Finset.Nat

public section


/-!
# USA Mathematical Olympiad 1988, Problem 3

Let X be the set {1, 2, ... , 20} and let P be the set of all 9-element
subsets of X. Show that for any map f : P → X we can find a 10-element
subset Y of X, such that f(Y - {k}) ≠ k for any k in Y.
-/

namespace Usa1988P3

open Finset

theorem usa1988_p3 (f : Finset ℕ → ℕ) :
    ∃ Y : Finset ℕ, Y ⊆ Finset.Icc 1 20 ∧ Y.card = 10 ∧
      ∀ k ∈ Y, f (Y.erase k) ≠ k := sorry

end Usa1988P3

File author(s): Kimi K3

This problem has a complete formalized solution.