OAI/GroupTheory/FiniteType/BoundaryValueBoundarySplit.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundaryValue.boundary_split line 26
2. lemma OAI.BoundaryValue.pivot_boundary_zero line 35
3. lemma OAI.BoundaryValue.replacement_boundary line 49
4. theorem OAI.BoundaryValue.boundary_zero line 110
5. structure OAI.FixedSingularTightening.System line 157
6. def OAI.FixedSingularTightening.topMap line 168
7. lemma OAI.FixedSingularTightening.boundary_compatible line 171
8. def OAI.FixedSingularTightening.boundaryHom line 187
9. lemma OAI.FixedSingularTightening.boundaryHom_zero line 192
10. lemma OAI.FixedSingularTightening.boundaryHom_one line 198
11. theorem OAI.FixedSingularTightening.exists_next line 203
12. def OAI.FixedSingularTightening.next line 216
13. lemma OAI.FixedSingularTightening.next_zero line 220
14. lemma OAI.FixedSingularTightening.next_face line 227
15. lemma OAI.FixedSingularTightening.next_top line 241
16. lemma OAI.FixedSingularTightening.next_fixed line 248
17. def OAI.FixedSingularTightening.extendHom line 252
18. lemma OAI.FixedSingularTightening.extendHom_old line 260
19. lemma OAI.FixedSingularTightening.extendHom_new line 265
20. def OAI.FixedSingularTightening.extend line 269
21. theorem OAI.FixedSingularTightening.exists_baseHom line 305
22. def OAI.FixedSingularTightening.baseHom line 316
23. def OAI.FixedSingularTightening.base line 320
24. def OAI.FixedSingularTightening.system line 341
25. def OAI.FixedSingularTightening.hom line 346
26. lemma OAI.FixedSingularTightening.hom_zero line 350
27. lemma OAI.FixedSingularTightening.hom_top line 354
28. lemma OAI.FixedSingularTightening.hom_face line 358
29. lemma OAI.FixedSingularTightening.hom_fixed line 368