OAI/GroupTheory/FiniteType/PresentationGeometryCellCoverExtension.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PresentationGeometry.CellCoverExtension.oldLift_isEmbedding line 24
  2. lemma OAI.PresentationGeometry.CellCoverExtension.range_oldLift line 31
  3. def OAI.PresentationGeometry.CellCoverExtension.boundarySlice line 41
  4. def OAI.PresentationGeometry.CellCoverExtension.sphereInDisk line 45
  5. def OAI.PresentationGeometry.CellCoverExtension.attachedDisk line 48
  6. lemma OAI.PresentationGeometry.CellCoverExtension.attachedDisk_boundary line 53
  7. lemma OAI.PresentationGeometry.CellCoverExtension.attaching_lift_nullhomotopic line 57
  8. def OAI.AffineChains.vertices line 83
  9. abbrev OAI.AffineChains.chains line 89
  10. def OAI.AffineChains.generator line 93
  11. lemma OAI.AffineChains.generator_boundary line 96
  12. def OAI.AffineChains.desc line 101
  13. lemma OAI.AffineChains.generator_desc line 104
  14. lemma OAI.AffineChains.hom_ext line 109
  15. def OAI.AffineChains.verticesMap line 113
  16. def OAI.AffineChains.map line 117
  17. lemma OAI.AffineChains.generator_map line 120
  18. def OAI.AffineChains.cone line 124
  19. lemma OAI.AffineChains.generator_cone line 127
  20. lemma OAI.AffineChains.cons_face_zero line 130
  21. lemma OAI.AffineChains.cons_face_succ line 135
  22. lemma OAI.AffineChains.cone_boundary_zero line 142
  23. lemma OAI.AffineChains.cone_boundary_succ line 158
  24. lemma OAI.AffineChains.boundary_constant line 177
  25. def OAI.AffineChains.subdiv line 188
  26. lemma OAI.AffineChains.subdiv_zero line 193
  27. lemma OAI.AffineChains.generator_subdiv_succ line 195
  28. lemma OAI.AffineChains.subdiv_comm line 200
  29. def OAI.AffineChains.subdivision line 222
  30. def OAI.AffineChains.prism line 225
  31. lemma OAI.AffineChains.prism_zero line 232
  32. lemma OAI.AffineChains.generator_prism_succ line 234
  33. lemma OAI.AffineChains.prism_boundary line 240
  34. lemma OAI.AffineChains.map_cone line 274
  35. lemma OAI.AffineChains.subdiv_map line 290
  36. lemma OAI.AffineChains.prism_map line 305