OAI/Topology/CoarseAssembly/RipsFiniteHomotopy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Whole-union invariance for finitely supported analytic homotopies

The representations may vary throughout the homotopy. Finitely many changing components give the uniform continuity required by the actual Roe algebra.

  1. theorem OAI.CoarseAssembly.uniform_continuity_of_finite_variation line 18
  2. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_finiteHomotopy line 43