OAI/GroupTheory/FiniteType/SingularSupport.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SingularSupport.gen line 13
2. def OAI.SingularSupport.span line 15
3. lemma OAI.SingularSupport.gen_mem line 18
4. lemma OAI.SingularSupport.span_mono line 21
5. lemma OAI.SingularSupport.map_mem line 26
6. lemma OAI.SingularSupport.induction_on line 35
7. lemma OAI.SingularSupport.map_gen line 53
8. lemma OAI.SingularSupport.boundary_gen line 56
9. abbrev OAI.SmallChains.Small line 67
10. def OAI.SmallChains.group line 69
11. lemma OAI.SmallChains.small_comp line 71
12. lemma OAI.SmallChains.gen_mem line 76
13. lemma OAI.SmallChains.boundary_mem line 79
14. lemma OAI.SmallChains.realize_mem line 89
15. lemma OAI.SmallChains.subdiv_mem line 100
16. lemma OAI.SmallChains.prism_mem line 108
17. def OAI.AffineMesh.center line 122
18. def OAI.AffineMesh.ratio line 124
19. lemma OAI.AffineMesh.ratio_nonneg line 126
20. lemma OAI.AffineMesh.ratio_lt_one line 127
21. lemma OAI.AffineMesh.ratio_mono line 130
22. lemma OAI.AffineMesh.center_mem_hull line 136
23. lemma OAI.AffineMesh.center_sub line 143
24. lemma OAI.AffineMesh.center_dist_vertex line 152
25. lemma OAI.AffineMesh.center_dist_hull line 170
26. lemma OAI.AffineMesh.hull_dist line 180
27. instance OAI.ConvexSimplex.stdMetricSpace line 198
28. def OAI.SubdivisionMesh.InHull line 210
29. def OAI.SubdivisionMesh.MeshLe line 214
30. def OAI.SubdivisionMesh.Good line 216
31. lemma OAI.SubdivisionMesh.hull_self line 219
32. lemma OAI.SubdivisionMesh.hull_face_subset line 222
33. lemma OAI.SubdivisionMesh.center_hull line 227
34. lemma OAI.SubdivisionMesh.center_dist_hull line 233
35. lemma OAI.SubdivisionMesh.good_cone line 242
36. theorem OAI.SubdivisionMesh.subdiv_mesh line 264
37. def OAI.SubdivisionMesh.iterate line 292
38. lemma OAI.SubdivisionMesh.subdiv_mem line 297
39. lemma OAI.SubdivisionMesh.iterate_mesh line 304
40. lemma OAI.SubdivisionMesh.basis_mesh line 313