OAI/Topology/CoarseAssembly/DiscConnected.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Connectivity of the triangular lattice discs

Moving a nonzero coordinate one step toward zero stays in the hexagonal disc and decreases the sum of absolute coordinates. This gives paths to the origin within each finite base disc.

  1. def OAI.CoarseAssembly.discOrigin line 16
  2. def OAI.CoarseAssembly.discRank line 18
  3. theorem OAI.CoarseAssembly.disc_lower_neighbor line 20
  4. theorem OAI.CoarseAssembly.disc_reachable_origin line 89
  5. theorem OAI.CoarseAssembly.discGraph_connected line 99