OAI/Geometry/SingularHomology/SingularSubdivisionSupport.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SingularSubdivision.carried line 11
  2. theorem OAI.Problem340.SingularSubdivision.mem_carried line 14
  3. theorem OAI.Problem340.SingularSubdivision.generator_mem_carried_iff line 17
  4. theorem OAI.Problem340.SingularSubdivision.generator_mem_carried line 22
  5. theorem OAI.Problem340.SingularSubdivision.carried_eq_span line 26
  6. theorem OAI.Problem340.SingularSubdivision.carried_mono line 30
  7. theorem OAI.Problem340.SingularSubdivision.map_mem_of_carried_generators line 34
  8. theorem OAI.Problem340.SingularSubdivision.face_mem_carrier line 45
  9. theorem OAI.Problem340.SingularSubdivision.boundary_mem_carried line 49
  10. theorem OAI.Problem340.SingularSubdivision.cone_mem_carried line 57
  11. theorem OAI.Problem340.SingularSubdivision.mapVertices_mem_carried line 66
  12. theorem OAI.Problem340.SingularSubdivision.mapVertices_mem_carried_image line 74
  13. def OAI.Problem340.SingularSubdivision.CentersIn line 79
  14. theorem OAI.Problem340.SingularSubdivision.subdivision_mem_carried line 82
  15. theorem OAI.Problem340.SingularSubdivision.subdivisionHomotopy_mem_carried line 95
  16. theorem OAI.Problem340.SingularSubdivision.iterate_subdivision_mem_carried line 111
  17. theorem OAI.Problem340.SingularSubdivision.iterate_subdivision_support line 120
  18. theorem OAI.Problem340.SingularSubdivision.carried_cycle_subdivision_difference line 128