OAI/Combinatorics/TriangleRemoval/Tracking/PrefixEmbeddings.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.prefixEmbeddings line 21
  2. lemma OAI.SharpTerminalLeave.mem_prefixEmbeddings line 28
  3. def OAI.SharpTerminalLeave.dropLastEmbedding line 33
  4. lemma OAI.SharpTerminalLeave.dropLastEmbedding_apply line 37
  5. lemma OAI.SharpTerminalLeave.dropLastEmbedding_mem line 41
  6. def OAI.SharpTerminalLeave.compatibleNext line 49
  7. lemma OAI.SharpTerminalLeave.embedding_fiber_le line 54
  8. theorem OAI.SharpTerminalLeave.prefixEmbeddings_succ_bound line 81
  9. lemma OAI.SharpTerminalLeave.prefixEmbeddings_zero line 92
  10. theorem OAI.SharpTerminalLeave.prefixEmbeddings_product_bound line 99
  11. theorem OAI.SharpTerminalLeave.compatibleNext_le_codegree line 117
  12. theorem OAI.SharpTerminalLeave.compatibleNext_le_degree line 132
  13. lemma OAI.SharpTerminalLeave.compatibleNext_le_order line 142