OAI/Topology/CoarseAssembly/BoundaryLoopMaps.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The same boundary family maps to the filled base and detected total space

The source class is defined on the actual boundary Rips complex. Its base image is identified with the previously constructed filled loop family.

  1. theorem OAI.CoarseAssembly.totalToFiber_dist line 40
  2. def OAI.CoarseAssembly.boundaryLoops line 42
  3. def OAI.CoarseAssembly.boundaryLoopStage line 46
  4. def OAI.CoarseAssembly.boundaryLoopClass line 51
  5. def OAI.CoarseAssembly.boundaryComponentToBase line 55
  6. theorem OAI.CoarseAssembly.boundaryComponentToBase_nonexpanding line 58
  7. def OAI.CoarseAssembly.concreteBaseWalk line 63
  8. theorem OAI.CoarseAssembly.boundaryLoop_base line 67
  9. theorem OAI.CoarseAssembly.boundaryFamily_toBase line 74
  10. theorem OAI.CoarseAssembly.boundaryLoopStage_base_zero line 101
  11. def OAI.CoarseAssembly.realFiberLoops line 111
  12. def OAI.CoarseAssembly.fiberLoopsOne line 121
  13. def OAI.CoarseAssembly.realFiberStage line 123
  14. theorem OAI.CoarseAssembly.realFiberStage_cast line 129
  15. theorem OAI.CoarseAssembly.boundaryLoop_fiber line 138
  16. theorem OAI.CoarseAssembly.boundaryFamily_toFiber line 151