OAI/MathematicalPhysics/Heisenberg/HullComponents.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.LatticeCut.Boundary line 12
  2. def OAI.Heisenberg.LatticeCut.outer line 15
  3. lemma OAI.Heisenberg.LatticeCut.step_to_shift line 18
  4. lemma OAI.Heisenberg.LatticeCut.cut_mem_iff line 23
  5. lemma OAI.Heisenberg.LatticeCut.outer_boundary line 27
  6. lemma OAI.Heisenberg.LatticeCut.boundary_has_cut line 35
  7. lemma OAI.Heisenberg.LatticeCut.square_outer_bounds line 42
  8. lemma OAI.Heisenberg.LatticeCut.linked_outer_near line 57
  9. theorem OAI.Heisenberg.LatticeCut.boundary_connected line 66
  10. lemma OAI.Heisenberg.Geometry.ball_symm line 82
  11. lemma OAI.Heisenberg.Geometry.ball_triangle line 86
  12. lemma OAI.Heisenberg.Geometry.ball_mono line 93
  13. lemma OAI.Heisenberg.Geometry.ball_self line 96
  14. lemma OAI.Heisenberg.Geometry.ball_connected line 99
  15. lemma OAI.Heisenberg.Geometry.step_ball_one line 109
  16. lemma OAI.Heisenberg.Geometry.interpolate_near line 116
  17. def OAI.Heisenberg.LatticeComponents.Component line 125
  18. def OAI.Heisenberg.LatticeComponents.Thick line 128
  19. lemma OAI.Heisenberg.LatticeComponents.thick_mono line 131
  20. lemma OAI.Heisenberg.LatticeComponents.self_mem_component line 136
  21. lemma OAI.Heisenberg.LatticeComponents.component_closed line 139
  22. lemma OAI.Heisenberg.LatticeComponents.component_symmetric line 143
  23. lemma OAI.Heisenberg.LatticeComponents.component_eq_of_mem line 152
  24. lemma OAI.Heisenberg.LatticeComponents.components_disjoint line 158
  25. lemma OAI.Heisenberg.LatticeComponents.thickenings_disjoint line 165
  26. lemma OAI.Heisenberg.LatticeComponents.overlapping_balls line 175
  27. lemma OAI.Heisenberg.LatticeComponents.thick_component_connected line 185
  28. lemma OAI.Heisenberg.LatticeComponents.boundary_unit_clear line 208
  29. theorem OAI.Heisenberg.LatticeComponents.surviving_boundary_connected line 222
  30. lemma OAI.Heisenberg.Geometry.exterior_ball_connected line 242
  31. lemma OAI.Heisenberg.Geometry.ball_finite line 252
  32. lemma OAI.Heisenberg.Geometry.ball_enlarge_step line 258
  33. lemma OAI.Heisenberg.Geometry.interpolate_near_confined line 262