OAI/Combinatorics/Chromatic/Walls/TriangularScheduledRoots.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularOmega_skew line 12
  2. lemma OAI.ElementaryPositivity.TriangularDynamics.omega_anchors line 16
  3. lemma OAI.ElementaryPositivity.TriangularDynamics.omega_delta_anchor line 22
  4. lemma OAI.ElementaryPositivity.TriangularDynamics.omega_anchor_delta line 26
  5. lemma OAI.ElementaryPositivity.TriangularDynamics.omega_delta_delta line 30
  6. def OAI.ElementaryPositivity.TriangularDynamics.levelCartan line 34
  7. lemma OAI.ElementaryPositivity.TriangularDynamics.levelCartan_comm line 37
  8. lemma OAI.ElementaryPositivity.TriangularDynamics.omega_delta_bridge line 40
  9. lemma OAI.ElementaryPositivity.TriangularDynamics.omega_event_delta line 50
  10. def OAI.ElementaryPositivity.TriangularDynamics.scheduledBridge line 56
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.scheduledBridge_self line 59
  12. lemma OAI.ElementaryPositivity.TriangularDynamics.scheduledRoot_anchor line 63
  13. lemma OAI.ElementaryPositivity.TriangularDynamics.scheduledRoot_bridge line 71
  14. def OAI.ElementaryPositivity.PathLattice.gap line 111
  15. def OAI.ElementaryPositivity.PathLattice.roots line 113
  16. lemma OAI.ElementaryPositivity.PathLattice.roots_apply line 116
  17. def OAI.ElementaryPositivity.PathLattice.coord line 119
  18. lemma OAI.ElementaryPositivity.PathLattice.coord_apply line 122
  19. lemma OAI.ElementaryPositivity.PathLattice.coord_single line 129
  20. lemma OAI.ElementaryPositivity.PathLattice.coord_gap line 137
  21. lemma OAI.ElementaryPositivity.PathLattice.coord_roots line 143
  22. lemma OAI.ElementaryPositivity.PathLattice.roots_injective line 154
  23. lemma OAI.ElementaryPositivity.PathLattice.gaps_linearIndependent line 159
  24. def OAI.ElementaryPositivity.PathLattice.weight line 165
  25. lemma OAI.ElementaryPositivity.PathLattice.weight_apply line 166
  26. lemma OAI.ElementaryPositivity.PathLattice.weight_single line 167
  27. lemma OAI.ElementaryPositivity.PathLattice.weight_gap line 169
  28. lemma OAI.ElementaryPositivity.PathLattice.weight_roots line 171