OAI/Topology/CoarseAssembly/RegularizedCoarsening.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit regularization is compatible with Rips coarsening

  1. theorem OAI.CoarseAssembly.Rips.ControlledCycleFamily.eq_of_cycles_bound line 19
  2. theorem OAI.CoarseAssembly.Rips.regularizedFamily_coarsen line 28
  3. theorem OAI.CoarseAssembly.Rips.regularizedFamily_boundary_coarsen line 37