OAI/Topology/CoarseAssembly/RegularizedRipsRelations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The regularized whole-union boundary respects all analytic cycle relations

  1. theorem OAI.CoarseAssembly.Rips.regularizedFamily_unitary line 18
  2. theorem OAI.CoarseAssembly.Rips.regularizedFamily_directSum line 29
  3. theorem OAI.CoarseAssembly.Rips.regularizedFamily_degenerate line 43