OAI/Combinatorics/RamseyFive/Streams/PermutationCylinder.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.PermutationCylinder.Cylinder line 9
2. instance OAI.SharpRamseyFive.PermutationCylinder.cylinderFintype line 12
3. lemma OAI.SharpRamseyFive.PermutationCylinder.preserves_complement line 16
4. def OAI.SharpRamseyFive.PermutationCylinder.remainingEquiv line 28
5. theorem OAI.SharpRamseyFive.PermutationCylinder.card_cylinder line 54
6. def OAI.SharpRamseyFive.PermutationCylinder.nextReference line 59
7. lemma OAI.SharpRamseyFive.PermutationCylinder.nextReference_at line 63
8. lemma OAI.SharpRamseyFive.PermutationCylinder.nextReference_old line 67
9. def OAI.SharpRamseyFive.PermutationCylinder.stepEquiv line 75
10. theorem OAI.SharpRamseyFive.PermutationCylinder.card_next line 90
11. theorem OAI.SharpRamseyFive.PermutationCylinder.next_probability line 97