05 Combinatorics

TheoremErdős–Ko–Rado theorem#

The Erdős–Ko–Rado theorem.

The maximum size of an intersecting family in α where all sets have size r is bounded by (card α - 1).choose (r - 1). This bound is sharp.

Finset.erdos_ko_rado {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (↑𝒜).Intersecting)
  (h₂ : Set.Sized r ↑𝒜) (h₃ : r ≤ n / 2) : 𝒜.card ≤ (n - 1).choose (r - 1)
Sources
MathlibFinset.erdos_ko_rado
Uses 5
Statement usesFinite set · Natural number
Proof usesFormula for the Number of Combinations · Integer · Kruskal-Katona theorem

TheoremHindman's theorem (1000+ theorems)#

The strong form of Hindman's theorem: in any finite cover of an FP-set, one the parts contains an FP-set.

Hindman.FP_partition_regular.{u_1} {M : Type u_1} [Semigroup M] (a : Stream' M) (s : Set (Set M))
  (sfin : s.Finite) (scov : ∀ (m : M), Hindman.FP a m → m ∈ ⋃₀ s) :
  ∃ c ∈ s, ∃ b, ∀ (m : M), Hindman.FP b m → m ∈ c
Sources
MathlibHindman.FP_partition_regular
Uses 4
Statement usesStream
Proof usesCompactness in terms of filters · Continuous function · Hausdorff space

TheoremMultinomial theorem#

The multinomial theorem.

Finset.sum_pow_eq_sum_piAntidiag_of_commute.{u_1, u_2} {α : Type u_1} {R : Type u_2} [DecidableEq α]
  [Semiring R] (s : Finset α) (f : α → R) (hc : (↑s).Pairwise (Function.onFun Commute f)) (n : ℕ) :
  (∑ i ∈ s, f i) ^ n =
    ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
Sources
MathlibFinset.sum_pow_eq_sum_piAntidiag_of_commute
Uses 2
Statement usesFinite set · Natural number

TheoremTutte theorem#

Tutte's theorem

A graph has a perfect matching if and only if: For every subset u of vertices, removing this subset induces at most u.ncard components of odd size. This is formally stated using the predicate IsTutteViolator, which is satisfied exactly when this condition does not hold.

SimpleGraph.tutte.{u_1} {V : Type u_1} {G : SimpleGraph V} [Finite V] :
  (∃ M, M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
Sources
MathlibSimpleGraph.tutte
Uses 5
Statement usesCardinal · Matching · Natural number · Ring morphism
Proof usesDegree-sum formula

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.