OAI/Topology/CoarseAssembly/RipsFamilyMap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Proper maps from componentwise compact families into Rips realizations

The boundary family will be a countable family of parametrized circles. Compact subsets of the target use finitely many vertices, hence meet only finitely many members of this family. This proves properness directly.

  1. theorem OAI.CoarseAssembly.separatedRipsMap_continuous line 23
  2. theorem OAI.CoarseAssembly.separatedRipsMap_weight line 30
  3. def OAI.CoarseAssembly.ripsFamilyContinuousMap line 38
  4. theorem OAI.CoarseAssembly.ripsFamily_preimage_compact line 48
  5. def OAI.CoarseAssembly.ripsFamilyMap line 73
  6. theorem OAI.CoarseAssembly.ripsFamilyMap_coarsen line 83