OAI/Combinatorics/TriangleRemoval/Embeddings/RerootTemplate.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.rerootTemplate line 13
  2. lemma OAI.SharpTerminalLeave.rerootTemplate_image_subset line 19
  3. lemma OAI.SharpTerminalLeave.rerootTemplate_remaining line 24
  4. def OAI.SharpTerminalLeave.RootedTwoBalanced line 41
  5. lemma OAI.SharpTerminalLeave.balanced_overlap_scale line 45
  6. lemma OAI.SharpTerminalLeave.balanced_completion_bound line 54
  7. theorem OAI.SharpTerminalLeave.balanced_reroot_completion_bound line 69
  8. lemma OAI.SharpTerminalLeave.fintype_sum_le_injection line 87
  9. abbrev OAI.SharpTerminalLeave.RootedEdgePin line 97
  10. lemma OAI.SharpTerminalLeave.rootedEdgePin_card line 103
  11. def OAI.SharpTerminalLeave.rootedEdgeFiberEncoding line 118
  12. lemma OAI.SharpTerminalLeave.rootedEdgeFiberEncoding_injective line 132
  13. lemma OAI.SharpTerminalLeave.intact_antitone_required line 140
  14. lemma OAI.SharpTerminalLeave.rooted_edge_fiber_load line 149
  15. theorem OAI.SharpTerminalLeave.rooted_copyEdgeLoad_from_reroots line 169
  16. theorem OAI.SharpTerminalLeave.balanced_rooted_load_bound line 199