OAI/MathematicalPhysics/Heisenberg/LatticeHulls.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Geometry.exists_box line 10
  2. lemma OAI.Heisenberg.Geometry.exterior_to_shell line 16
  3. lemma OAI.Heisenberg.Geometry.exterior_connected line 50
  4. lemma OAI.Heisenberg.Geometry.reach_end_mem line 69
  5. lemma OAI.Heisenberg.Geometry.ambient_connected line 75
  6. def OAI.Heisenberg.LatticeHull.Hull line 83
  7. lemma OAI.Heisenberg.LatticeHull.subset_hull line 86
  8. lemma OAI.Heisenberg.LatticeHull.complement_connected line 90
  9. lemma OAI.Heisenberg.LatticeHull.inner_endpoint_mem line 102
  10. lemma OAI.Heisenberg.LatticeHull.hull_connected line 108
  11. lemma OAI.Heisenberg.LatticeHull.hull_subset_box line 130
  12. lemma OAI.Heisenberg.LatticeHull.base_independence line 139
  13. lemma OAI.Heisenberg.LatticeHull.box_finite line 148
  14. lemma OAI.Heisenberg.LatticeHull.finite_contained_box line 154
  15. lemma OAI.Heisenberg.LatticeHull.hull_finite line 167
  16. lemma OAI.Heisenberg.LatticeHull.exterior_iff_unbounded line 172
  17. lemma OAI.Heisenberg.LatticeHull.reach_preserves_hull line 199
  18. lemma OAI.Heisenberg.LatticeHull.connected_avoids_hull line 207
  19. lemma OAI.Heisenberg.LatticeHull.hull_subset_of_subset_hull line 217
  20. theorem OAI.Heisenberg.LatticeHull.hull_laminar line 228