OAI/Combinatorics/Ryser/Construction/PoolThinProbability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.Construction.poolThinLaw line 19
2. def OAI.RyserCoveringCounterexample.Construction.poolGroupBad line 23
3. def OAI.RyserCoveringCounterexample.Construction.poolBadGroups line 29
4. def OAI.RyserCoveringCounterexample.Construction.PoolThin line 33
5. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_poolGroupBad_le line 37
6. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_poolGroupBad_le_of_card line 60
7. theorem OAI.RyserCoveringCounterexample.Construction.poolThinLaw_prob_all_bad_le line 70
8. theorem OAI.RyserCoveringCounterexample.Construction.poolThinLaw_prob_six_bad_le line 97
9. theorem OAI.RyserCoveringCounterexample.Construction.prob_not_poolThin_le line 136