OAI/Combinatorics/BalancedRyser/Candidates/ExposedExternalSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ExposedExternalSum.externalEvent line 16
2. def OAI.Balanced.ExposedExternalSum.oldOldSum line 21
3. theorem OAI.Balanced.ExposedExternalSum.oldOldSum_le line 26
4. def OAI.Balanced.ExposedExternalSum.freshDirections line 61
5. theorem OAI.Balanced.ExposedExternalSum.freshDirections_card_le line 64
6. def OAI.Balanced.ExposedExternalSum.oldFreshSum line 71
7. theorem OAI.Balanced.ExposedExternalSum.oldFreshSum_le_div line 76
8. theorem OAI.Balanced.ExposedExternalSum.oldFreshSum_le line 128
9. theorem OAI.Balanced.ExposedExternalSum.old_external_total_le line 133