OAI/Topology/CoarseAssembly/BoundaryComponents.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact boundary components in the actual boundary metric

The disjoint family of finite boundary vertex sets is isometric to the depth-zero subtype used for the spatial boundary maps.

  1. def OAI.CoarseAssembly.boundaryComponentMetric line 18
  2. def OAI.CoarseAssembly.boundaryComponentsMetric line 23
  3. def OAI.CoarseAssembly.boundaryReindex line 28
  4. theorem OAI.CoarseAssembly.boundaryReindex_dist line 34
  5. theorem OAI.CoarseAssembly.boundaryEdgeBound line 52
  6. def OAI.CoarseAssembly.boundaryFamilyMap line 63