OAI/Combinatorics/IndependentSets/Geometry/GeometryLocations.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LargeIndependentSets.GeometryNames.Outcome line 16
  2. abbrev OAI.LargeIndependentSets.GeometryNames.outcomeCount line 17
  3. abbrev OAI.LargeIndependentSets.GeometryNames.vertexCount line 18
  4. lemma OAI.LargeIndependentSets.GeometryNames.vertexCount_pos line 20
  5. def OAI.LargeIndependentSets.GeometryNames.vertexEquiv line 23
  6. def OAI.LargeIndependentSets.GeometryNames.scheduleLC line 26
  7. def OAI.LargeIndependentSets.GeometryNames.samplePoint line 29
  8. lemma OAI.LargeIndependentSets.GeometryNames.samplePoint_decode line 33
  9. def OAI.LargeIndependentSets.GeometryNames.locationName line 38
  10. lemma OAI.LargeIndependentSets.GeometryNames.locationName_exact line 43
  11. def OAI.LargeIndependentSets.GeometryNames.vertexCountExpr line 48
  12. def OAI.LargeIndependentSets.GeometryNames.outcomeExpr line 49
  13. def OAI.LargeIndependentSets.GeometryNames.chainExpr line 50
  14. lemma OAI.LargeIndependentSets.GeometryNames.vertexCountExpr_eval line 54
  15. lemma OAI.LargeIndependentSets.GeometryNames.chainExpr_eval line 58
  16. lemma OAI.LargeIndependentSets.GeometryNames.outcomeExpr_eval line 64
  17. def OAI.LargeIndependentSets.GeometryNames.scheduleTest line 73
  18. lemma OAI.LargeIndependentSets.GeometryNames.scheduleTest_nonzero line 77
  19. def OAI.LargeIndependentSets.GeometryNames.scheduleCodeExpr line 103
  20. lemma OAI.LargeIndependentSets.GeometryNames.scheduleCodeExpr_eval line 106
  21. def OAI.LargeIndependentSets.GeometryNames.samplePointExpr line 113
  22. lemma OAI.LargeIndependentSets.GeometryNames.samplePointExpr_eval line 117
  23. def OAI.LargeIndependentSets.GeometryNames.tupleCodeExpr line 126
  24. lemma OAI.LargeIndependentSets.GeometryNames.tupleCodeExpr_eval line 129
  25. def OAI.LargeIndependentSets.GeometryNames.locationExpr line 135
  26. lemma OAI.LargeIndependentSets.GeometryNames.locationExpr_eval line 141