OAI/Topology/CoarseAssembly/RipsEmbedding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Simplicial embeddings and isolated Rips components

An injective nonexpanding vertex map induces the actual barycentric map. For an isometric component separated from its complement at the Rips scale, its realization is a clopen subspace. Finite components are compact, so the inclusion is proper.

  1. theorem OAI.CoarseAssembly.Rips.mapPoint_weight_self line 23
  2. theorem OAI.CoarseAssembly.Rips.mapPoint_continuous line 27
  3. theorem OAI.CoarseAssembly.Rips.mapPoint_injective line 43
  4. theorem OAI.CoarseAssembly.Rips.coarsen_mapPoint line 51
  5. theorem OAI.CoarseAssembly.Rips.mapPoint_range line 56
  6. theorem OAI.CoarseAssembly.Rips.mapPoint_range_open line 71
  7. theorem OAI.CoarseAssembly.Rips.mapPoint_closedEmbedding line 87
  8. def OAI.CoarseAssembly.Rips.componentInclusion line 91