OAI/Topology/CoarseAssembly/RipsUnrestrictedHomotopy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary componentwise analytic homotopies preserve the Rips boundary

Only the endpoint cycle families need uniform operator bounds. The rational transform gives norm-one intermediate operators, and finite telescoping allows arbitrary componentwise speeds.

  1. theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_homotopy line 22