OAI/Combinatorics/Ryser/LineCover/TwoPopulationSampling.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RyserCoveringCounterexample.InjectionSampling.card_pairSample_relation_leline 18 - theorem
OAI.RyserCoveringCounterexample.InjectionSampling.prob_restrict_productline 40 - theorem
OAI.RyserCoveringCounterexample.InjectionSampling.prob_pairSample_relation_leline 64 - theorem
OAI.RyserCoveringCounterexample.InjectionSampling.prob_restricted_relation_leline 95 - theorem
OAI.RyserCoveringCounterexample.InjectionSampling.prob_relation_matching_leline 112