OAI/Combinatorics/Chromatic/Walls/ForwardChartMutation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ElementaryPositivity.TriangularDynamics.FreeChart line 14
  2. def OAI.ElementaryPositivity.TriangularDynamics.FreeChart.mutate line 20
  3. lemma OAI.ElementaryPositivity.TriangularDynamics.freeChart_inventory_step line 27
  4. lemma OAI.ElementaryPositivity.ForwardChain.gaps_ofFn_nodes line 53
  5. lemma OAI.ElementaryPositivity.TriangularDynamics.levelNode_zero line 71
  6. lemma OAI.ElementaryPositivity.TriangularDynamics.levelNode_last line 73
  7. lemma OAI.ElementaryPositivity.TriangularDynamics.levelNode_middle line 75
  8. def OAI.ElementaryPositivity.TriangularDynamics.gapIndices line 81
  9. lemma OAI.ElementaryPositivity.TriangularDynamics.mem_gapIndices line 83
  10. lemma OAI.ElementaryPositivity.TriangularDynamics.gapIndices_nodup line 86
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.initial_levelGaps line 97
  12. lemma OAI.ElementaryPositivity.TriangularDynamics.initial_forwardInventory line 106
  13. lemma OAI.ElementaryPositivity.TriangularDynamics.simpleRoot_forwardRoots line 115
  14. abbrev OAI.ElementaryPositivity.LatticeExtension.Extended line 131
  15. def OAI.ElementaryPositivity.LatticeExtension.dot line 133
  16. lemma OAI.ElementaryPositivity.LatticeExtension.dot_apply line 138
  17. lemma OAI.ElementaryPositivity.LatticeExtension.dot_add line 139
  18. lemma OAI.ElementaryPositivity.LatticeExtension.dot_zero line 141
  19. lemma OAI.ElementaryPositivity.LatticeExtension.dot_single line 142
  20. def OAI.ElementaryPositivity.LatticeExtension.form line 146
  21. lemma OAI.ElementaryPositivity.LatticeExtension.form_apply line 153
  22. lemma OAI.ElementaryPositivity.LatticeExtension.form_self line 156
  23. def OAI.ElementaryPositivity.LatticeExtension.includeVertices line 165
  24. lemma OAI.ElementaryPositivity.LatticeExtension.includeVertices_apply line 167
  25. lemma OAI.ElementaryPositivity.LatticeExtension.includeVertices_injective line 169
  26. lemma OAI.ElementaryPositivity.LatticeExtension.form_original line 172
  27. lemma OAI.ElementaryPositivity.LatticeExtension.form_nondegenerate line 176