OAI/Analysis/SphereIsometry/SubdivisionRestriction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The exact original-face restriction of every concrete subdivision

  1. def OAI.Tingley.iterEmbedding line 14
  2. theorem OAI.Tingley.iterEmbedding_carrier line 19
  3. theorem OAI.Tingley.iterEmbedding_range_iff line 31
  4. theorem OAI.Tingley.iterEmbedding_faceCarrier line 43
  5. theorem OAI.Tingley.iterEmbedding_face_range_iff line 50
  6. def OAI.Tingley.lastFaceEmbedding line 56
  7. theorem OAI.Tingley.lastFace_carrier line 59
  8. theorem OAI.Tingley.lastFace_faceCarrier line 64
  9. theorem OAI.Tingley.lastFace_range_iff line 69
  10. theorem OAI.Tingley.lastFace_mem_iff line 77
  11. theorem OAI.Tingley.lastFace_face_range_iff line 81
  12. theorem OAI.Tingley.lastFace_map_top_mem line 91
  13. theorem OAI.Tingley.lastFace_top_image line 97