OAI/Combinatorics/BalancedRyser/Probability/FreshDoublePrescription.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.FreshCoordinate.probability_two_prescriptions_on_subtype line 15
2. def OAI.Balanced.FreshTupleWitness.orientedExternalPair line 47
3. theorem OAI.Balanced.FreshTupleWitness.oriented_external_pair_probability_on_event line 54
4. def OAI.Balanced.FreshTupleWitness.successWithPoint line 81
5. theorem OAI.Balanced.FreshTupleWitness.successWithPoint_update_fresh line 88
6. theorem OAI.Balanced.FreshTupleWitness.successful_external_pair_probability_on_event line 95
7. theorem OAI.Balanced.FreshTupleWitness.exposedLaw_eq_uniform_fiber line 112
8. theorem OAI.Balanced.FreshTupleWitness.successful_external_pair_probability_exposed line 129