OAI/Combinatorics/Coboundary/Cosets.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.Vertex line 16
2. instance OAI.CoboundaryExpanders.TypedCosetFaces.(instance at line 17) line 17
3. def OAI.CoboundaryExpanders.TypedCosetFaces.vertex line 18
4. def OAI.CoboundaryExpanders.TypedCosetFaces.face line 19
5. def OAI.CoboundaryExpanders.TypedCosetFaces.types line 20
6. def OAI.CoboundaryExpanders.TypedCosetFaces.IsFace line 21
7. def OAI.CoboundaryExpanders.TypedCosetFaces.stabilizer line 22
8. theorem OAI.CoboundaryExpanders.TypedCosetFaces.mem_stabilizer line 25
9. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertex_injective line 29
10. theorem OAI.CoboundaryExpanders.TypedCosetFaces.face_card line 34
11. theorem OAI.CoboundaryExpanders.TypedCosetFaces.types_face line 37
12. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertex_mem line 41
13. lemma OAI.CoboundaryExpanders.TypedCosetFaces.face_eq_iff line 54
14. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.FaceOfType line 76
15. def OAI.CoboundaryExpanders.TypedCosetFaces.quotientFace line 78
16. lemma OAI.CoboundaryExpanders.TypedCosetFaces.quotientFace_bijective line 84
17. def OAI.CoboundaryExpanders.TypedCosetFaces.faceEquiv line 98
18. lemma OAI.CoboundaryExpanders.TypedCosetFaces.faceEquiv_mk line 101
19. abbrev OAI.CoboundaryExpanders.TypedCosetFaces.Remaining line 115
20. def OAI.CoboundaryExpanders.TypedCosetFaces.linkGroups line 117
21. def OAI.CoboundaryExpanders.TypedCosetFaces.linkVertex line 120
22. lemma OAI.CoboundaryExpanders.TypedCosetFaces.linkVertex_vertex line 129
23. lemma OAI.CoboundaryExpanders.TypedCosetFaces.linkVertex_injective line 133
24. lemma OAI.CoboundaryExpanders.TypedCosetFaces.linkVertex_type_not_mem line 147
25. lemma OAI.CoboundaryExpanders.TypedCosetFaces.linkFace_image line 150
26. def OAI.CoboundaryExpanders.TypedCosetFaces.IsLinkFace line 154
27. lemma OAI.CoboundaryExpanders.TypedCosetFaces.types_of_mem line 157
28. lemma OAI.CoboundaryExpanders.TypedCosetFaces.face_subset_iff line 161
29. theorem OAI.CoboundaryExpanders.TypedCosetFaces.isLinkFace_iff line 172
30. theorem OAI.CoboundaryExpanders.TypedCosetFaces.linkFace_iff line 230
31. def OAI.CoboundaryExpanders.TypedCosetFaces.isoVertex line 246
32. lemma OAI.CoboundaryExpanders.TypedCosetFaces.isoVertex_vertex line 255
33. lemma OAI.CoboundaryExpanders.TypedCosetFaces.isoVertex_injective line 259
34. lemma OAI.CoboundaryExpanders.TypedCosetFaces.isoVertex_surjective line 274
35. def OAI.CoboundaryExpanders.TypedCosetFaces.vertexEquiv line 281
36. lemma OAI.CoboundaryExpanders.TypedCosetFaces.isoFace_image line 286
37. theorem OAI.CoboundaryExpanders.TypedCosetFaces.isoFace_iff line 290
38. def OAI.CoboundaryExpanders.TypedCosetFaces.vertexLinkGroups line 308
39. def OAI.CoboundaryExpanders.TypedCosetFaces.singleStabilizerEquiv line 311
40. def OAI.CoboundaryExpanders.TypedCosetFaces.singleTypesEquiv line 314
41. lemma OAI.CoboundaryExpanders.TypedCosetFaces.singletonGroups_correspond line 318
42. def OAI.CoboundaryExpanders.TypedCosetFaces.vertexLinkEmbedding line 322
43. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexLinkEmbedding_injective line 327
44. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexLinkEmbedding_vertex line 331
45. theorem OAI.CoboundaryExpanders.TypedCosetFaces.vertexLinkFace_iff line 334
46. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexLinkFace_surjective line 339
47. lemma OAI.CoboundaryExpanders.TypedCosetFaces.subset_face line 360
48. lemma OAI.CoboundaryExpanders.TypedCosetFaces.IsFace.downward line 376
49. def OAI.CoboundaryExpanders.TypedCosetFaces.complex line 380
50. def OAI.CoboundaryExpanders.TypedCosetFaces.linkComplex line 385
51. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexPath_common line 407
52. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexPath_symm line 412
53. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexPath_mul line 419
54. lemma OAI.CoboundaryExpanders.TypedCosetFaces.vertexPath_of_generate line 440