OAI/Analysis/IrrationalRotation/Rotation/CircleParameterBlocks.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterData.blockEnd_zero line 9
2. theorem OAI.Invariant233.CircleParameterData.blockEnd_succ line 12
3. theorem OAI.Invariant233.CircleParameterData.card_block line 16
4. theorem OAI.Invariant233.CircleParameterData.mem_block_iff line 24
5. theorem OAI.Invariant233.CircleParameterData.blockEnd_ge_index line 28
6. theorem OAI.Invariant233.CircleParameterData.blockEnd_strictMono line 37
7. theorem OAI.Invariant233.CircleParameterData.exists_mem_block line 44
8. theorem OAI.Invariant233.CircleParameterData.block_index_unique line 60
9. theorem OAI.Invariant233.CircleParameterData.blockIndex_eq_of_mem line 76
10. theorem OAI.Invariant233.CircleParameterData.blockIndex_pos line 91
11. theorem OAI.Invariant233.CircleParameterData.flattenedCost_eq_of_mem line 97