OAI/Geometry/SingularHomology/TetrahedronGoodCover.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SimplicialSphere.vertexStar line 11
  2. def OAI.Problem340.SimplicialSphere.starIntersection line 14
  3. lemma OAI.Problem340.SimplicialSphere.isOpen_vertexStar line 17
  4. lemma OAI.Problem340.SimplicialSphere.vertexStar_cover line 21
  5. lemma OAI.Problem340.SimplicialSphere.starIntersection_univ line 33
  6. def OAI.Problem340.SimplicialSphere.starAmbient line 41
  7. def OAI.Problem340.SimplicialSphere.faceCenter line 44
  8. lemma OAI.Problem340.SimplicialSphere.faceCenter_mem_simplex line 47
  9. lemma OAI.Problem340.SimplicialSphere.faceCenter_pos line 56
  10. lemma OAI.Problem340.SimplicialSphere.faceCenter_mem_starAmbient line 61
  11. lemma OAI.Problem340.SimplicialSphere.starAmbient_starConvex line 71
  12. def OAI.Problem340.SimplicialSphere.starIntersectionHomeomorph line 91
  13. theorem OAI.Problem340.SimplicialSphere.contractible_starIntersection line 115
  14. lemma OAI.Problem340.SimplicialSphere.starIntersection_eq_biInter line 122
  15. lemma OAI.Problem340.SimplicialSphere.isOpen_starIntersection line 127
  16. lemma OAI.Problem340.SimplicialSphere.starIntersection_nonempty line 131
  17. theorem OAI.Problem340.SimplicialSphere.starIntersection_nonempty_iff line 138
  18. lemma OAI.Problem340.SimplicialSphere.vertexStar_list_nonempty_iff line 151
  19. theorem OAI.Problem340.SimplicialSphere.contractible_starPreimage line 173
  20. lemma OAI.Problem340.SimplicialSphere.exists_coordinate_ge_quarter line 179
  21. theorem OAI.Problem340.SimplicialSphere.exists_ball_subset_vertexStar line 191
  22. theorem OAI.Problem340.SimplicialSphere.subset_vertexStar_of_pairwise_dist_lt line 206