OAI/Combinatorics/TriangleRemoval/Process/PathSuffix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathUnion_ancestor_closed line 22
  2. def OAI.SharpTerminalLeave.TriangleGrowth.pathSuffix line 30
  3. lemma OAI.SharpTerminalLeave.TriangleGrowth.mem_pathSuffix line 33
  4. lemma OAI.SharpTerminalLeave.TriangleGrowth.within_pathSuffix line 37
  5. theorem OAI.SharpTerminalLeave.TriangleGrowth.pathSuffix_covered line 51
  6. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathSuffix_mark line 64
  7. theorem OAI.SharpTerminalLeave.TriangleGrowth.pathSuffix_sparse line 70
  8. theorem OAI.SharpTerminalLeave.TriangleGrowth.injective_path_collision line 80