OAI/Topology/CoarseAssembly/ExplicitPersistence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Persistence of the explicit circle cycle in the actual graph union

  1. theorem OAI.CoarseAssembly.ripsFamily_restriction_class line 14
  2. def OAI.CoarseAssembly.explicitFiberLoops line 36
  3. def OAI.CoarseAssembly.explicitFiberStage line 40
  4. theorem OAI.CoarseAssembly.explicitFiberStage_coarsen line 44
  5. theorem OAI.CoarseAssembly.explicitFiberStage_detected line 55
  6. def OAI.CoarseAssembly.explicitFiberClass line 82
  7. theorem OAI.CoarseAssembly.explicitFiberClass_infinite_order line 85