OAI/Combinatorics/TriangleRemoval/Embeddings/PathBirthIndex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.reindexSet_pair line 21
  2. lemma OAI.SharpTerminalLeave.PathForest.restrict_parent_none line 34
  3. lemma OAI.SharpTerminalLeave.TriangleGrowth.suffix_eq_ordered line 45
  4. def OAI.SharpTerminalLeave.TriangleGrowth.pathBirthIndex line 47
  5. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathBirthIndex_val line 52
  6. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathBirthIndex_embedding line 55
  7. def OAI.SharpTerminalLeave.TriangleGrowth.pathAttachments line 61
  8. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathAttachments_eq line 65
  9. def OAI.SharpTerminalLeave.TriangleGrowth.pathRootEdges line 72
  10. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathForest_parent_some line 75
  11. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathForest_parent_none line 84
  12. theorem OAI.SharpTerminalLeave.TriangleGrowth.pathAttachments_valid line 92