OAI/Combinatorics/ThinTrees/Continuation/Pencil.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Continuation pencil.

  1. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Form line 16
  2. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.qdiff line 18
  3. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.qlap line 20
  4. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.qtriangle line 23
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.qproject line 28
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_qdiff line 30
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_qinc line 33
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_qlap line 35
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_qtriangle line 37
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_qproject line 40
  11. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.matrixForm line 47
  12. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.lowerForm line 51
  13. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.upperForm line 54
  14. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.edgeForm line 58
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.real_matrixForm line 62
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.real_lowerForm line 74
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.real_upperForm line 78
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.real_edgeForm line 89
  19. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.MatBlock line 96
  20. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.matrixBlocks line 98
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.matrixBlocks_symmetric line 103
  22. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.ScalarBlock line 122
  23. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.capacityForm line 125
  24. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.scalarForms line 128
  25. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.order line 147
  26. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.rowIndex line 149
  27. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.affineMatrix line 159
  28. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.affineMatrix_symmetric line 164
  29. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.continuationPencil line 185