OAI/Combinatorics/BalancedRyser/Probability/UniformSubsetExposure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.uniform_product_event_probability line 11
2. theorem OAI.Balanced.uniform_two_subsets_contains_probability line 29
3. theorem OAI.Balanced.uniform_expected_filtered_card line 44
4. theorem OAI.Balanced.uncovered_iff_incident_subset line 55
5. theorem OAI.Balanced.uniform_two_subsets_expected_uncovered_card line 68