OAI/Topology/CoarseAssembly/RipsCompactSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact subsets of a locally finite Rips complex

A compact set of probability weights has its entire support in one finite vertex set. The proof uses a finite cover by positive-coordinate stars and the finite metric balls around those coordinates.

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