OAI/Topology/CoarseAssembly/SeparatedCoarseAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Constructed coarse assembly for the separated finite-component application

The maps are defined on actual locally finite analytic K-homology and are compatible with coarsening by the proved finite-tail argument.

  1. theorem OAI.CoarseAssembly.Rips.separatedIndexFamily_atScale line 22
  2. def OAI.CoarseAssembly.Rips.separatedCoarseAssembly line 35
  3. theorem OAI.CoarseAssembly.Rips.separatedCoarseAssembly_of line 45