OAI/Combinatorics/ThinTrees/Continuation/Coordinates.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Continuation coordinates.

  1. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Triple line 15
  2. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Var line 16
  3. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.dimension line 19
  4. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.index line 21
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.matIndex line 31
  6. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.mulIndex line 32
  7. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.edgeIndex line 33
  8. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.flowIndex line 34
  9. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.rawMatrix line 37
  10. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.multiplier line 39
  11. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.y line 41
  12. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.z line 42
  13. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.flowX line 43
  14. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.flowA line 44
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.flowB line 45
  16. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.step line 47
  17. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.flow line 49
  18. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.rational line 52
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.rational_real line 55
  20. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode line 58
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_mat line 66
  22. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_mul line 68
  23. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_y line 70
  24. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_z line 72
  25. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_x line 74
  26. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_a line 76
  27. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_b line 78
  28. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_step line 81
  29. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_flow line 93
  30. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.close_step_flow line 99
  31. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.encode_bound line 119
  32. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.dimension_bound line 133