OAI/Combinatorics/Ryser/Construction/GadgetOriginalDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Construction.prob_originalLineCount_lt_five line 20
2. theorem OAI.RyserCoveringCounterexample.Construction.not_originalLineDensity_imp_exists_small_count line 79
3. theorem OAI.RyserCoveringCounterexample.Construction.prob_not_originalLineDensity_le line 89
4. theorem OAI.RyserCoveringCounterexample.Construction.prob_originalLineDensity_ge line 116
5. theorem OAI.RyserCoveringCounterexample.Construction.tendsto_originalDensity_failure_atTop line 124
6. def OAI.RyserCoveringCounterexample.Construction.originalDensityProbability line 133
7. theorem OAI.RyserCoveringCounterexample.Construction.tendsto_originalDensityProbability line 136