OAI/Combinatorics/Chromatic/Walls/TriangularLinearSection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.TriangularDynamics.extendedCoord_anchor_zero line 15
  2. lemma OAI.ElementaryPositivity.TriangularDynamics.rootOrder_anchor_zero line 20
  3. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularLinear_initial line 24
  4. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularLinear_theta line 37
  5. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularLinear_negative_theta line 47
  6. def OAI.ElementaryPositivity.TriangularDynamics.pureAnchor line 68
  7. lemma OAI.ElementaryPositivity.TriangularDynamics.pureAnchor_apply_anchor line 71
  8. lemma OAI.ElementaryPositivity.TriangularDynamics.pureAnchor_apply_bridge line 73
  9. lemma OAI.ElementaryPositivity.TriangularDynamics.anchor_pair_pure line 76
  10. lemma OAI.ElementaryPositivity.TriangularDynamics.bridge_pair_pure line 88
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularSeed_dominant_nonnegative line 96
  12. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularPure_incoming line 113
  13. lemma OAI.ElementaryPositivity.TriangularDynamics.pureAnchor_of_bridges_zero line 139
  14. lemma OAI.ElementaryPositivity.TriangularDynamics.bridges_zero_of_level_zero line 146
  15. lemma OAI.ElementaryPositivity.TriangularDynamics.triangularSeed_order_nonnegative line 160
  16. theorem OAI.ElementaryPositivity.TriangularDynamics.triangularPure_detect line 168