OAI/Combinatorics/BalancedRyser/Probability/UncoveredExchange.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.UncoveredExchange.missed line 11
2. lemma OAI.Balanced.UncoveredExchange.missed_subset line 15
3. lemma OAI.Balanced.UncoveredExchange.missed_insert line 19
4. lemma OAI.Balanced.UncoveredExchange.abs_card_filter_not_sub_le line 26
5. theorem OAI.Balanced.UncoveredExchange.missed_exchange_bound line 40
6. theorem OAI.Balanced.UncoveredExchange.plane_exchange_bound line 57
7. lemma OAI.Balanced.UncoveredExchange.missed_line line 69
8. theorem OAI.Balanced.UncoveredExchange.target_exchange_bound line 74
9. theorem OAI.Balanced.UncoveredExchange.normalized_plane_exchange_bound line 90
10. theorem OAI.Balanced.UncoveredExchange.normalized_target_exchange_bound line 101