OAI/Topology/CoarseAssembly/BoundaryGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The concrete proper boundary inclusions

The boundary is the depth-zero vertex subset with the induced metric from the total graph family. Its projection to the base is nonexpanding. These are the actual two vertex inclusions used for assembly naturality.

  1. theorem OAI.CoarseAssembly.walk_image_dist_le line 21
  2. theorem OAI.CoarseAssembly.fiberProjection_nonexpanding line 33
  3. theorem OAI.CoarseAssembly.vertexProjection_nonexpanding line 47
  4. def OAI.CoarseAssembly.boundaryMetric line 65
  5. theorem OAI.CoarseAssembly.boundaryToVertex_nonexpanding line 69
  6. theorem OAI.CoarseAssembly.boundaryToBase_nonexpanding line 75