OAI/Combinatorics/TriangleRemoval/Process/BornEdges.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.BirthGraph.bornEdges line 20
  2. def OAI.SharpTerminalLeave.BirthGraph.backEdges line 23
  3. theorem OAI.SharpTerminalLeave.BirthGraph.pair_injective_on_older line 26
  4. theorem OAI.SharpTerminalLeave.BirthGraph.bornEdges_card line 38
  5. theorem OAI.SharpTerminalLeave.BirthGraph.bornEdges_disjoint line 41
  6. theorem OAI.SharpTerminalLeave.BirthGraph.backEdges_card line 57
  7. theorem OAI.SharpTerminalLeave.BirthGraph.backEdges_mem_pair line 64
  8. theorem OAI.SharpTerminalLeave.BirthGraph.backEdges_card_le line 71
  9. theorem OAI.SharpTerminalLeave.BirthGraph.backEdges_card_eq line 77
  10. def OAI.SharpTerminalLeave.BirthGraph.inducedEdges line 82
  11. theorem OAI.SharpTerminalLeave.BirthGraph.inducedEdges_eq line 85
  12. theorem OAI.SharpTerminalLeave.BirthGraph.inducedEdges_card_le line 98
  13. theorem OAI.SharpTerminalLeave.BirthGraph.inducedEdges_sparse line 105
  14. theorem OAI.SharpTerminalLeave.BirthGraph.induced_plus_one_sparse line 126