OAI/Combinatorics/BalancedRyser/Construction/ExternalWitnessPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ExternalAssembly.swapKey line 13
2. theorem OAI.Balanced.ExternalAssembly.swapKey_swapKey line 17
3. theorem OAI.Balanced.ExternalAssembly.witnessEvent_swapKey line 22
4. theorem OAI.Balanced.ExternalAssembly.swapKey_mem_witnesses line 31
5. theorem OAI.Balanced.ExternalAssembly.filter_card_swapKey line 35
6. theorem OAI.Balanced.ExternalAssembly.card_le_bothFresh_add_twice_firstOld line 51
7. theorem OAI.Balanced.ExternalAssembly.firstOld_card_eq_three_cases line 71
8. theorem OAI.Balanced.ExternalAssembly.card_le_four_cases line 84
9. theorem OAI.Balanced.ExternalAssembly.integral_card_le_four_cases line 97