OAI/MathematicalPhysics/Heisenberg/HullRouting.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.LatticeHull.hull_subset_ball line 10
  2. lemma OAI.Heisenberg.LatticeHull.boundary_subset_ball line 19
  3. lemma OAI.Heisenberg.LatticeHull.boundary_nonempty line 24
  4. lemma OAI.Heisenberg.LatticeComponents.thick_finite line 43
  5. lemma OAI.Heisenberg.LatticeComponents.component_finite line 49
  6. lemma OAI.Heisenberg.LatticeComponents.thick_nonempty line 52
  7. lemma OAI.Heisenberg.LatticeComponents.hull_cut_clearance line 55
  8. theorem OAI.Heisenberg.LatticeComponents.surviving_boundary_confined line 77
  9. def OAI.Heisenberg.HullRouting.DisjointFamily line 101
  10. lemma OAI.Heisenberg.HullRouting.member_unique line 104
  11. def OAI.Heisenberg.HullRouting.collapse line 110
  12. lemma OAI.Heisenberg.HullRouting.collapse_of_mem line 113
  13. lemma OAI.Heisenberg.HullRouting.collapse_free line 120
  14. lemma OAI.Heisenberg.HullRouting.collapse_survives line 123
  15. def OAI.Heisenberg.HullRouting.RouteRegion line 131
  16. lemma OAI.Heisenberg.HullRouting.region_boundary line 135
  17. theorem OAI.Heisenberg.HullRouting.route_exists line 141
  18. def OAI.Heisenberg.HullRouting.allHulls line 182
  19. def OAI.Heisenberg.HullRouting.maxHulls line 185
  20. lemma OAI.Heisenberg.HullRouting.mem_allHulls line 188
  21. lemma OAI.Heisenberg.HullRouting.mem_maxHulls line 192
  22. lemma OAI.Heisenberg.HullRouting.allHulls_laminar line 197
  23. lemma OAI.Heisenberg.HullRouting.maxHulls_disjoint line 210
  24. lemma OAI.Heisenberg.HullRouting.maxHulls_cover line 220
  25. lemma OAI.Heisenberg.HullRouting.allHulls_boundary_nonempty line 230
  26. theorem OAI.Heisenberg.HullRouting.finite_hull_routing line 239
  27. lemma OAI.Heisenberg.HullRouting.exists_exterior_base line 281