OAI/Topology/CoarseAssembly/FiniteRips.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compactness of finite Rips realizations

The finite Rips complex is a closed subset of the compact probability simplex. In particular, its circle test has a compact domain.

  1. theorem OAI.CoarseAssembly.Rips.range_coordinates line 22
  2. theorem OAI.CoarseAssembly.Rips.coordinates_closed line 53
  3. theorem OAI.CoarseAssembly.Rips.coordinates_compact line 67
  4. instance OAI.CoarseAssembly.Rips.(instance at line 78) line 78