OAI/Topology/CoarseAssembly/RipsMapCalculus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact naturality of the parametrized Rips paths

Injective nonexpanding vertex maps commute with barycentric interpolation, edge paths and concatenated graph walks, including their parametrizations.

  1. theorem OAI.CoarseAssembly.Rips.mapPoint_weight line 22
  2. theorem OAI.CoarseAssembly.Rips.mapPoint_comp line 25
  3. theorem OAI.CoarseAssembly.Rips.mapPoint_vertex line 31
  4. theorem OAI.CoarseAssembly.Rips.mapPoint_interpolate line 36
  5. theorem OAI.CoarseAssembly.Rips.mapPoint_edgePath line 58
  6. theorem OAI.CoarseAssembly.Rips.mapPoint_walkPath line 70
  7. theorem OAI.CoarseAssembly.Rips.mapPoint_loopCircle line 87