OAI/Combinatorics/HoneycombCorridor/BoundaryContainment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.faceIndicator line 12
  2. theorem OAI.PolynomialVacuumBridge.Corridor.faceBoundary_local line 14
  3. theorem OAI.PolynomialVacuumBridge.Corridor.faceBoundaryWord_local line 29
  4. theorem OAI.PolynomialVacuumBridge.Corridor.faceBoundaryWord_gradient line 44
  5. theorem OAI.PolynomialVacuumBridge.Corridor.finite_indicator_row_containment line 61
  6. theorem OAI.PolynomialVacuumBridge.Corridor.star_boundary_potential_contained line 112
  7. theorem OAI.PolynomialVacuumBridge.Corridor.contour_unused_advance line 131
  8. theorem OAI.PolynomialVacuumBridge.Corridor.star_boundary_trace_outside line 139
  9. theorem OAI.PolynomialVacuumBridge.Corridor.star_boundary_endpoint line 147