OAI/GroupTheory/FiniteType/CoveringCellGeometryHausdorff.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CoveringCellGeometry.hausdorff line 16
  2. lemma OAI.PresentationGeometry.Cells.skeleton_eq_old line 36
  3. lemma OAI.CoveringCW.skeleton_preimage line 63
  4. lemma OAI.SingularChains.homologyMap_of_homotopic line 87
  5. lemma OAI.SingularChains.homologyMap_const_zero line 92
  6. lemma OAI.PresentationGeometry.CellCoverExtension.attaching_homology_killed line 114
  7. lemma OAI.PresentationGeometry.CellCoverExtension.oldLift_skeleton line 126
  8. lemma OAI.PresentationGeometry.CellCoverExtension.oldLift_homology_surjective line 139
  9. lemma OAI.PresentationGeometry.CellCoverExtension.oldLift_homology_bijective line 147
  10. def OAI.CoreDeck.right line 162
  11. lemma OAI.CoreDeck.right_proj line 165
  12. lemma OAI.CoreDeck.right_chart line 169
  13. lemma OAI.CoreDeck.continuous_right line 179
  14. def OAI.CoreDeck.homeo line 194
  15. lemma OAI.CoreDeck.of_potential line 211
  16. instance OAI.CoreDeck.action line 216
  17. theorem OAI.CoreDeck.continuousAction line 231
  18. lemma OAI.CoreDeck.transitive_fiber line 235
  19. lemma OAI.CoreDeck.right_free line 245