OAI/Combinatorics/PolynomialVacuum/Bridge/NestingSystems.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.mem_polygonSystems line 7
  2. theorem OAI.PolynomialVacuumBridge.Corridor.empty_mem_polygonSystems line 14
  3. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.not_vertices_subset_interior line 18
  4. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.not_mutually_nested line 23
  5. theorem OAI.PolynomialVacuumBridge.Corridor.polygonSystem_outermost line 32
  6. theorem OAI.PolynomialVacuumBridge.Corridor.polygonSystem_erase_outermost line 46
  7. theorem OAI.PolynomialVacuumBridge.Corridor.not_mem_interior_system line 61
  8. theorem OAI.PolynomialVacuumBridge.Corridor.polygonSystem_insert_outer line 67
  9. theorem OAI.PolynomialVacuumBridge.Corridor.polygonSystem_insert_unique line 101
  10. def OAI.PolynomialVacuumBridge.Corridor.outerSystems line 116
  11. theorem OAI.PolynomialVacuumBridge.Corridor.polygonSystems_split line 120
  12. theorem OAI.PolynomialVacuumBridge.Corridor.outerSystems_disjoint line 145
  13. theorem OAI.PolynomialVacuumBridge.Corridor.empty_not_mem_outerSystems line 159
  14. theorem OAI.PolynomialVacuumBridge.Corridor.faceNestingMass_recursion line 165