OAI/Combinatorics/Ryser/Construction/PoolThinGeometry.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.RyserCoveringCounterexample.Construction.ShiftHitsline 15 - def
OAI.RyserCoveringCounterexample.Construction.badShiftsline 20 - theorem
OAI.RyserCoveringCounterexample.Construction.mem_badShiftsline 25 - theorem
OAI.RyserCoveringCounterexample.Construction.badShifts_eq_biUnionline 31 - theorem
OAI.RyserCoveringCounterexample.Construction.badShifts_card_leline 57 - theorem
OAI.RyserCoveringCounterexample.Construction.uniform_prob_shiftHits_leline 82