OAI/Combinatorics/BalancedRyser/Local/LocalUnusedTripleProbability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.Local.UnusedTripleProbability.unusedOffsets line 17
2. theorem OAI.Balanced.Local.UnusedTripleProbability.prescribedDesignated_card_le line 21
3. theorem OAI.Balanced.Local.UnusedTripleProbability.prescribedDesignated_eq_of_used_agreement line 28
4. theorem OAI.Balanced.Local.UnusedTripleProbability.unusedNoncollinearTriple_imp line 37
5. theorem OAI.Balanced.Local.UnusedTripleProbability.refreshed_unusedNoncollinearTriple_probability_le line 60
6. theorem OAI.Balanced.Local.UnusedTripleProbability.mixed_unusedNoncollinearTriple_probability_le line 88