OAI/Combinatorics/HoneycombCorridor/PotentialSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.rationalFlowComponent line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.conserved_finite_potential line 13
  3. theorem OAI.PolynomialVacuumBridge.Corridor.potential_supported_on_cycle_cells line 39
  4. theorem OAI.PolynomialVacuumBridge.Corridor.edge_mem_around line 94
  5. theorem OAI.PolynomialVacuumBridge.Corridor.incident_faces_equal line 103
  6. theorem OAI.PolynomialVacuumBridge.Corridor.nonboundary_vertex_all_edges line 112
  7. theorem OAI.PolynomialVacuumBridge.Corridor.finite_vertex_flat_zero line 130
  8. theorem OAI.PolynomialVacuumBridge.Corridor.flat_along_dart line 157
  9. theorem OAI.PolynomialVacuumBridge.Corridor.cell_flat_zero_boundary line 165