OAI/GroupTheory/ArtinCAT0/Detour.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArtinCAT0.GridDisk.rounded_edge_bound line 11
2. lemma OAI.ArtinCAT0.GridDisk.cone_fill line 20
3. abbrev OAI.ArtinCAT0.SixSector.AngularSize line 59
4. def OAI.ArtinCAT0.SixSector.angularEquiv line 61
5. lemma OAI.ArtinCAT0.SixSector.angularEquiv_val line 63
6. lemma OAI.ArtinCAT0.SixSector.angularEquiv_add line 64
7. lemma OAI.ArtinCAT0.SixSector.angularEquiv_one line 70
8. def OAI.ArtinCAT0.SixSector.circleAt line 75
9. def OAI.ArtinCAT0.SixSector.innerLabel line 78
10. lemma OAI.ArtinCAT0.SixSector.circleAt_zero line 82
11. lemma OAI.ArtinCAT0.SixSector.circleAt_step line 93
12. lemma OAI.ArtinCAT0.SixSector.innerLabel_edges line 98
13. lemma OAI.ArtinCAT0.SixSector.innerLabel_chart line 123
14. def OAI.ArtinCAT0.RayIndex.shifted line 138
15. lemma OAI.ArtinCAT0.RayIndex.edge_chain_equal line 140
16. lemma OAI.ArtinCAT0.TriangleMesh.Replacement.edgeFlux_equal line 154
17. lemma OAI.ArtinCAT0.SixSector.chart_plane_other_uniform line 168
18. lemma OAI.ArtinCAT0.SixSector.ringCircle_next_product line 177
19. lemma OAI.ArtinCAT0.SixSector.circle_shift_diagonal line 186
20. lemma OAI.ArtinCAT0.SixSector.circle_chain_index line 197
21. lemma OAI.ArtinCAT0.SixSector.ringCircle_index line 237
22. lemma OAI.ArtinCAT0.GridDisk.sum_index_boundary line 253
23. lemma OAI.ArtinCAT0.SixSector.circleAt_index line 284
24. lemma OAI.ArtinCAT0.SixSector.innerLabel_index line 293
25. lemma OAI.ArtinCAT0.SixSector.cap_exists line 312
26. def OAI.ArtinCAT0.mirrorAt line 363
27. lemma OAI.ArtinCAT0.SixSector.refined_index_zero line 376
28. lemma OAI.ArtinCAT0.SixSector.circle_refined_side line 434
29. lemma OAI.ArtinCAT0.SixSector.refined_inner_index line 472
30. theorem OAI.ArtinCAT0.SixSector.no_strict_ratios line 521