Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1979P5

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
public import Mathlib.Algebra.Group.Action.Defs
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Ring.Nat

public section


/-!
# USA Mathematical Olympiad 1979, Problem 5

X has n members. Given n+1 subsets of X, each with 3 members,
show that we can always find two which have just one member in common.
-/

namespace Usa1979P5

open Finset

theorem usa1979_p5 {α : Type*} [DecidableEq α] (n : ℕ) (X : Finset α) (hX : X.card = n)
    (S : Finset (Finset α)) (hS : S.card = n + 1) (hsub : ∀ s ∈ S, s ⊆ X)
    (hcard : ∀ s ∈ S, s.card = 3) :
    ∃ s ∈ S, ∃ t ∈ S, s ≠ t ∧ (s ∩ t).card = 1 := sorry

end Usa1979P5

File author(s): Kimi K3

This problem has a complete formalized solution.