Documentation

LeanPool.ErdosTuzaValtr.Main.CapCup

LeanPool.ErdosTuzaValtr.Main.CapCup #

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.CapCup.

theorem Config.has_cap2_cup2 {α : Type u_1} [LinearOrder α] (C : Config α) {S : Finset α} (hS : 1 < S.card) :
C.HasNCap 2 S C.HasNCup 2 S
theorem Config.binom_eq (a b : ) :
(a + b + 2).choose (a + 1) = (a + b + 1).choose a + (a + b + 1).choose (a + 1)
theorem Config.cap_cup {α : Type u_1} [LinearOrder α] (C : Config α) (a b : ) (S : Finset α) (hS : (a + b).choose a < S.card) :
C.HasNCap (a + 2) S C.HasNCup (b + 2) S