OAI/Combinatorics/HoneycombCorridor/StripWindows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.vertexWindow line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.mem_vertexWindow line 14
  3. theorem OAI.PolynomialVacuumBridge.Corridor.vertexWindow_card_le line 21
  4. theorem OAI.PolynomialVacuumBridge.Corridor.bounded_position_mem_window line 32
  5. theorem OAI.PolynomialVacuumBridge.Corridor.strip_shell_card_le line 51
  6. theorem OAI.PolynomialVacuumBridge.Corridor.vertexWindow_convex line 66
  7. theorem OAI.PolynomialVacuumBridge.Corridor.bottomSource_mem_window line 87
  8. theorem OAI.PolynomialVacuumBridge.Corridor.vertexWindow_strip line 93
  9. theorem OAI.PolynomialVacuumBridge.Corridor.finite_vertices_in_window line 97