OAI/Combinatorics/Chromatic/Walls/FiniteLatticePairing.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.TriangularDynamics.matrixPairing line 12
  2. lemma OAI.ElementaryPositivity.TriangularDynamics.matrixPairing_apply line 17
  3. lemma OAI.ElementaryPositivity.TriangularDynamics.matrixPairing_single line 21
  4. lemma OAI.ElementaryPositivity.TriangularDynamics.matrixPairing_single_left line 25
  5. lemma OAI.ElementaryPositivity.TriangularDynamics.matrixPairing_skew line 33
  6. lemma OAI.ElementaryPositivity.TriangularDynamics.matrixPairing_self line 44
  7. def OAI.ElementaryPositivity.TriangularDynamics.chartMatrix line 51
  8. def OAI.ElementaryPositivity.TriangularDynamics.chartPairing line 59
  9. lemma OAI.ElementaryPositivity.TriangularDynamics.chartMatrix_skew line 63
  10. lemma OAI.ElementaryPositivity.TriangularDynamics.chartPairing_self line 72
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.total_as_sum line 78
  12. lemma OAI.ElementaryPositivity.TriangularDynamics.chartPairing_anchor line 96
  13. lemma OAI.ElementaryPositivity.TriangularDynamics.chartPairing_delta line 113
  14. lemma OAI.ElementaryPositivity.TriangularDynamics.chart_tropical_stationary line 122
  15. abbrev OAI.ElementaryPositivity.TriangularDynamics.Cell line 140
  16. def OAI.ElementaryPositivity.TriangularDynamics.cellLevel line 141
  17. def OAI.ElementaryPositivity.TriangularDynamics.cellRow line 142
  18. def OAI.ElementaryPositivity.TriangularDynamics.phaseEarlier line 144
  19. instance OAI.ElementaryPositivity.TriangularDynamics.(instance at line 146) line 146
  20. lemma OAI.ElementaryPositivity.TriangularDynamics.cell_ext line 149
  21. lemma OAI.ElementaryPositivity.TriangularDynamics.phaseEarlier_trichotomy line 158
  22. lemma OAI.ElementaryPositivity.TriangularDynamics.phaseEarlier_irrefl line 169
  23. lemma OAI.ElementaryPositivity.TriangularDynamics.phaseEarlier_asymm line 171
  24. def OAI.ElementaryPositivity.TriangularDynamics.bridgePositive line 180
  25. def OAI.ElementaryPositivity.TriangularDynamics.triangularBB line 184
  26. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularBB_skew line 186
  27. def OAI.ElementaryPositivity.TriangularDynamics.triangularOmega line 190
  28. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularOmega_self line 191
  29. lemma OAI.ElementaryPositivity.TriangularDynamics.eventRoot_anchor line 194
  30. lemma OAI.ElementaryPositivity.TriangularDynamics.eventRoot_bridge_value line 203