OAI/Combinatorics/MatchingCount/Graphs/TreeGeometry.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableSource.RawLogical line 11
  2. abbrev OAI.MatchingFPRAS.ExecutableSource.RawReal line 12
  3. abbrev OAI.MatchingFPRAS.ExecutableSource.RawVertex line 13
  4. abbrev OAI.MatchingFPRAS.ExecutableSource.GeometryInput line 14
  5. def OAI.MatchingFPRAS.ExecutableSource.logicalEdges line 16
  6. def OAI.MatchingFPRAS.ExecutableSource.logicalEdgesRealizer line 18
  7. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_logicalEdges line 20
  8. def OAI.MatchingFPRAS.ExecutableSource.internalCount line 27
  9. def OAI.MatchingFPRAS.ExecutableSource.internalCountRealizer line 28
  10. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_internalCount line 30
  11. lemma OAI.MatchingFPRAS.ExecutableSource.internalCount_bound line 32
  12. def OAI.MatchingFPRAS.ExecutableSource.realEdges line 36
  13. def OAI.MatchingFPRAS.ExecutableSource.realEdgesRealizer line 38
  14. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_realEdges line 41
  15. def OAI.MatchingFPRAS.ExecutableSource.vertices line 53
  16. def OAI.MatchingFPRAS.ExecutableSource.verticesRealizer line 55
  17. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_vertices line 59
  18. def OAI.MatchingFPRAS.ExecutableSource.position line 71
  19. def OAI.MatchingFPRAS.ExecutableSource.atRealizer line 75
  20. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_at line 82
  21. def OAI.MatchingFPRAS.ExecutableSource.left line 91
  22. def OAI.MatchingFPRAS.ExecutableSource.right line 92
  23. def OAI.MatchingFPRAS.ExecutableSource.leftRealizer line 93
  24. def OAI.MatchingFPRAS.ExecutableSource.rightRealizer line 94
  25. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_left line 96
  26. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_right line 101
  27. def OAI.MatchingFPRAS.ExecutableSource.logicalRepr line 110
  28. def OAI.MatchingFPRAS.ExecutableSource.realRepr line 111
  29. def OAI.MatchingFPRAS.ExecutableSource.vertexRepr line 112
  30. lemma OAI.MatchingFPRAS.ExecutableSource.logicalRepr_injective line 115
  31. lemma OAI.MatchingFPRAS.ExecutableSource.vertexRepr_injective line 119
  32. lemma OAI.MatchingFPRAS.ExecutableSource.at_repr line 131
  33. lemma OAI.MatchingFPRAS.ExecutableSource.left_repr line 135
  34. lemma OAI.MatchingFPRAS.ExecutableSource.right_repr line 138
  35. lemma OAI.MatchingFPRAS.ExecutableSource.mem_logicalEdges line 142
  36. lemma OAI.MatchingFPRAS.ExecutableSource.logicalRepr_mem line 146
  37. lemma OAI.MatchingFPRAS.ExecutableSource.logicalEdges_complete line 149
  38. lemma OAI.MatchingFPRAS.ExecutableSource.vertexRepr_mem line 153
  39. lemma OAI.MatchingFPRAS.ExecutableSource.vertices_complete line 161
  40. lemma OAI.MatchingFPRAS.ExecutableSource.realRepr_mem line 169
  41. lemma OAI.MatchingFPRAS.ExecutableSource.realEdges_complete line 172