OAI/Topology/CoarseAssembly/RipsProperEmbedding.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Proper simplicial maps induced by injective nonexpanding maps

This construction applies to the actual boundary inclusions. The closed range conditions record both the allowed vertices and all forbidden pairs in the source metric, so no finiteness of the whole source is required.

  1. theorem OAI.CoarseAssembly.Rips.mapPoint_embedding line 24
  2. theorem OAI.CoarseAssembly.Rips.range_mapPoint line 36
  3. theorem OAI.CoarseAssembly.Rips.mapPoint_properEmbedding line 75