OAI/Geometry/SingularHomology/SingularSubdivision.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SingularSubdivision.Chains line 11
  2. def OAI.Problem340.SingularSubdivision.generator line 13
  3. def OAI.Problem340.SingularSubdivision.face line 15
  4. def OAI.Problem340.SingularSubdivision.boundary line 18
  5. def OAI.Problem340.SingularSubdivision.cone line 22
  6. theorem OAI.Problem340.SingularSubdivision.boundary_generator line 25
  7. theorem OAI.Problem340.SingularSubdivision.cone_generator line 30
  8. theorem OAI.Problem340.SingularSubdivision.face_cons_zero line 34
  9. theorem OAI.Problem340.SingularSubdivision.face_cons_succ line 39
  10. theorem OAI.Problem340.SingularSubdivision.boundary_cone_generator line 47
  11. theorem OAI.Problem340.SingularSubdivision.linearMap_ext line 55
  12. theorem OAI.Problem340.SingularSubdivision.boundary_cone line 63
  13. theorem OAI.Problem340.SingularSubdivision.boundary_cone_zero line 71
  14. theorem OAI.Problem340.SingularSubdivision.boundary_boundary line 79
  15. abbrev OAI.Problem340.SingularSubdivision.Centers line 99
  16. def OAI.Problem340.SingularSubdivision.subdivision line 101
  17. theorem OAI.Problem340.SingularSubdivision.subdivision_zero line 106
  18. theorem OAI.Problem340.SingularSubdivision.subdivision_generator line 109
  19. theorem OAI.Problem340.SingularSubdivision.boundary_subdivision line 115
  20. def OAI.Problem340.SingularSubdivision.subdivisionHomotopy line 139
  21. theorem OAI.Problem340.SingularSubdivision.subdivisionHomotopy_zero line 146
  22. theorem OAI.Problem340.SingularSubdivision.subdivisionHomotopy_generator line 149
  23. theorem OAI.Problem340.SingularSubdivision.boundary_subdivisionHomotopy line 156
  24. theorem OAI.Problem340.SingularSubdivision.cycle_subdivision_difference line 190
  25. def OAI.Problem340.SingularSubdivision.mapVertices line 200
  26. theorem OAI.Problem340.SingularSubdivision.mapVertices_generator line 203
  27. theorem OAI.Problem340.SingularSubdivision.mapVertices_cone line 207
  28. theorem OAI.Problem340.SingularSubdivision.mapVertices_boundary line 219
  29. theorem OAI.Problem340.SingularSubdivision.mapVertices_subdivision line 230
  30. theorem OAI.Problem340.SingularSubdivision.mapVertices_subdivisionHomotopy line 245