OAI/GroupTheory/FiniteType/PresentationGeometryCellCoverExtensionAnyAttachingLiftNullhomotopic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PresentationGeometry.CellCoverExtension.any_attaching_lift_nullhomotopic line 16
  2. lemma OAI.PresentationGeometry.CellCoverExtension.any_attaching_homology_killed line 33
  3. lemma OAI.PresentationGeometry.CellCoverExtension.deck_attaching_homology_killed line 40
  4. def OAI.SimplexDisk.Fat line 54
  5. lemma OAI.SimplexDisk.closed line 56
  6. lemma OAI.SimplexDisk.convex line 63
  7. lemma OAI.SimplexDisk.bounded line 72
  8. lemma OAI.SimplexDisk.interior_nonempty line 80
  9. def OAI.SimplexDisk.fstEquiv line 98
  10. lemma OAI.SimplexDisk.exists_ambient line 138
  11. lemma OAI.SimplexDisk.interior_pos line 145
  12. def OAI.SimplexDisk.sumCLM line 152
  13. lemma OAI.SimplexDisk.sumCLM_apply line 154
  14. lemma OAI.SimplexDisk.sumCLM_surj line 157
  15. lemma OAI.SimplexDisk.interior_sum_lt line 162
  16. lemma OAI.SimplexDisk.fstEquiv_frontier line 172
  17. def OAI.SimplexDisk.ambient line 189
  18. lemma OAI.SimplexDisk.ambient_image line 191
  19. lemma OAI.SimplexDisk.ambient_frontier line 194
  20. def OAI.SimplexDisk.diskEquiv line 197
  21. lemma OAI.SimplexDisk.diskEquiv_val line 200
  22. lemma OAI.SimplexDisk.diskEquiv_boundary line 203
  23. lemma OAI.SimplexDisk.interior_of_pos line 210
  24. lemma OAI.SimplexDisk.diskEquiv_boundary_iff line 221