OAI/Combinatorics/Progressions/Estimates/BoundedFreeWords.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.freeWordSet_card_le line 11
2. theorem OAI.Erdos3.bchProductBracketSupport_card_le line 34
3. def OAI.Erdos3.BoundedFreeWord line 52
4. def OAI.Erdos3.boundedFreeWordCode line 56
5. theorem OAI.Erdos3.boundedFreeWordCode_injective line 61
6. instance OAI.Erdos3.boundedFreeWordFintype line 70
7. theorem OAI.Erdos3.boundedFreeWord_card_le line 73