OAI/Topology/CoarseAssembly/ProperGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Properness of the concrete coarse spaces

The proved finite-ball estimates imply compact closed balls in the actual shortest-path metrics. No completion or change of metric is involved.

  1. theorem OAI.CoarseAssembly.UniformFiniteBalls.properSpace line 16
  2. theorem OAI.CoarseAssembly.baseUnion_proper line 20
  3. theorem OAI.CoarseAssembly.vertexUnion_proper line 23