OAI/Combinatorics/PolynomialVacuum/Geometry/PolygonLaminar.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.facePointProduct line 7
  2. theorem OAI.PolynomialVacuumBridge.Corridor.facePointProduct_apply line 10
  3. theorem OAI.PolynomialVacuumBridge.Corridor.finite_face_potential_injective line 13
  4. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.germ_mem_vertices line 29
  5. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.level_constant_on_boundary line 37
  6. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.potential_constant_on_boundary line 52
  7. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.disjoint_potential_product line 62
  8. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.disjoint_common_face_nested line 87