OAI/Combinatorics/BalancedRyser/Candidates/OppositeCases.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Balanced.OppositeAssembly.Label line 14
2. def OAI.Balanced.OppositeAssembly.witnesses line 16
3. theorem OAI.Balanced.OppositeAssembly.mem_witnesses line 23
4. theorem OAI.Balanced.OppositeAssembly.exists_witness_of_opposite line 31
5. def OAI.Balanced.OppositeAssembly.freshWitnesses line 43
6. def OAI.Balanced.OppositeAssembly.oldFreshWitnesses line 47
7. theorem OAI.Balanced.OppositeAssembly.witnesses_subset_cases line 51
8. theorem OAI.Balanced.OppositeAssembly.witnesses_card_le_cases line 71
9. theorem OAI.Balanced.OppositeAssembly.oldFreshWitnesses_card_le line 81