OAI/Topology/CoarseAssembly/RipsFixedRepresentationHomotopy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform operator homotopies with fixed representations

The hypothesis controls the whole family's operator norm. Representation- varying homotopies and quotient descent are separate obligations.

  1. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_fixedRepresentationHomotopy line 21