OAI/Combinatorics/BalancedRyser/Probability/CylinderUnionBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BalancedRyser.at_least_subset_cylinder_union line 14
2. theorem OAI.BalancedRyser.measure_at_least_of_cylinder_bound line 30
3. theorem OAI.BalancedRyser.measureReal_at_least_of_cylinder_bound line 48
4. theorem OAI.BalancedRyser.measureReal_exists_at_least_of_cylinder_bound line 68
5. theorem OAI.BalancedRyser.subsingleton_predicate_cylinder_eq_or_empty line 92
6. theorem OAI.BalancedRyser.measure_subsingleton_predicate_cylinder line 114
7. theorem OAI.BalancedRyser.measureReal_subsingleton_predicate_cylinder line 127
8. theorem OAI.BalancedRyser.measureReal_at_least_subsingleton_predicates line 141