OAI/Combinatorics/TriangleRemoval/Spectral/EdgeStar.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.edgeStar line 21
  2. theorem OAI.SharpTerminalLeave.mem_edgeStar line 24
  3. def OAI.SharpTerminalLeave.neighborEdge line 27
  4. theorem OAI.SharpTerminalLeave.neighborEdge_injective line 30
  5. theorem OAI.SharpTerminalLeave.neighborEdge_surjective line 44
  6. def OAI.SharpTerminalLeave.neighborEdgeEquiv line 63
  7. theorem OAI.SharpTerminalLeave.edgeStar_card line 67
  8. theorem OAI.SharpTerminalLeave.edgeStar_exact_overlap line 72
  9. theorem OAI.SharpTerminalLeave.graph_star_error_norm line 82