OAI/Geometry/SingularHomology/BarycentricSubdivision.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SingularSubdivision.StandardSimplex line 11
  2. def OAI.Problem340.SingularSubdivision.simplexCenters line 13
  3. def OAI.Problem340.SingularSubdivision.standardVertices line 16
  4. def OAI.Problem340.SingularSubdivision.universalSubdivision line 18
  5. def OAI.Problem340.SingularSubdivision.universalHomotopy line 21
  6. lemma OAI.Problem340.SingularSubdivision.map_centers line 24
  7. lemma OAI.Problem340.SingularSubdivision.affine_centers line 30
  8. lemma OAI.Problem340.SingularSubdivision.standardVertices_face line 36
  9. theorem OAI.Problem340.SingularSubdivision.universalSubdivision_boundary line 42
  10. theorem OAI.Problem340.SingularSubdivision.universalHomotopy_boundary_zero line 54
  11. theorem OAI.Problem340.SingularSubdivision.universalHomotopy_boundary line 60
  12. lemma OAI.Problem340.SingularSubdivision.simplexCenters_zero line 74
  13. theorem OAI.Problem340.SingularSubdivision.subdivision_one line 81
  14. theorem OAI.Problem340.SingularSubdivision.subdivisionHomotopy_one line 93
  15. theorem OAI.Problem340.SingularSubdivision.universalSubdivision_zero line 102
  16. theorem OAI.Problem340.SingularSubdivision.universalHomotopy_zero line 106
  17. theorem OAI.Problem340.SingularSubdivision.mapVertices_universalSubdivision line 109
  18. theorem OAI.Problem340.SingularSubdivision.mapVertices_universalHomotopy line 119