OAI/Combinatorics/TriangleRemoval/Process/TerminalLaw.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpTerminalLeave.card_completeGraph line 13
  2. theorem OAI.SharpTerminalLeave.mem_completeGraph line 16
  3. theorem OAI.SharpTerminalLeave.mem_triangles line 20
  4. theorem OAI.SharpTerminalLeave.triangles_mono line 24
  5. theorem OAI.SharpTerminalLeave.triangle_edge_card line 30
  6. theorem OAI.SharpTerminalLeave.three_le_card_of_triangle line 35
  7. theorem OAI.SharpTerminalLeave.step_support_active line 41
  8. theorem OAI.SharpTerminalLeave.step_absorbing line 47
  9. theorem OAI.SharpTerminalLeave.step_support_subset line 51
  10. theorem OAI.SharpTerminalLeave.step_card_of_active line 59
  11. theorem OAI.SharpTerminalLeave.evolve_support_subset line 66
  12. theorem OAI.SharpTerminalLeave.evolve_card_of_active line 76
  13. theorem OAI.SharpTerminalLeave.evolve_terminal line 91
  14. theorem OAI.SharpTerminalLeave.terminal_support_subset line 99
  15. theorem OAI.SharpTerminalLeave.terminal_edges_have_two_vertices line 103
  16. theorem OAI.SharpTerminalLeave.terminal_triangle_free line 108
  17. theorem OAI.SharpTerminalLeave.terminal_card_le line 112
  18. theorem OAI.SharpTerminalLeave.delete_triangle_injective line 116
  19. theorem OAI.SharpTerminalLeave.step_uniform_triangle line 127
  20. theorem OAI.SharpTerminalLeave.evolve_absorbing line 143
  21. theorem OAI.SharpTerminalLeave.evolve_add line 149
  22. theorem OAI.SharpTerminalLeave.evolve_stable line 155