OAI/Combinatorics/Chromatic/Walls/PathRoot.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.PathLattice.roots_single line 11
  2. lemma OAI.ElementaryPositivity.PathLattice.roots_coord_single line 18
  3. lemma OAI.ElementaryPositivity.PathLattice.roots_coord line 35
  4. lemma OAI.ElementaryPositivity.PathLattice.coord_nonneg line 54
  5. lemma OAI.ElementaryPositivity.PathLattice.vertex_support_rootDegree line 60
  6. lemma OAI.ElementaryPositivity.PathLattice.gap_prefix_nonpositive line 71
  7. abbrev OAI.ElementaryPositivity.TriangularDynamics.GapIndex line 99
  8. def OAI.ElementaryPositivity.TriangularDynamics.levelNode line 101
  9. def OAI.ElementaryPositivity.TriangularDynamics.afterGap line 106
  10. lemma OAI.ElementaryPositivity.TriangularDynamics.afterGap_node line 111
  11. def OAI.ElementaryPositivity.TriangularDynamics.forwardGap line 124
  12. def OAI.ElementaryPositivity.TriangularDynamics.forwardCoord line 127
  13. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardCoord_apply line 130
  14. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardCoord_single line 137
  15. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardCoord_gap line 145
  16. def OAI.ElementaryPositivity.TriangularDynamics.forwardRoots line 168
  17. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardRoots_apply line 170
  18. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardCoord_roots line 174
  19. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardRoots_injective line 185
  20. lemma OAI.ElementaryPositivity.TriangularDynamics.forwardGap_independent line 190