OAI/Combinatorics/IndependentSets/Geometry/GeometryLink.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.GeometryNames.pointCost line 14
  2. lemma OAI.LargeIndependentSets.GeometryNames.copyCost_same line 19
  3. def OAI.LargeIndependentSets.GeometryNames.questionExpr line 44
  4. lemma OAI.LargeIndependentSets.GeometryNames.questionExpr_nonzero line 51
  5. def OAI.LargeIndependentSets.GeometryNames.pointStepExpr line 79
  6. lemma OAI.LargeIndependentSets.GeometryNames.pointStepExpr_eval line 83
  7. def OAI.LargeIndependentSets.GeometryNames.forwardExpr line 94
  8. lemma OAI.LargeIndependentSets.GeometryNames.forwardExpr_nonzero line 99
  9. def OAI.LargeIndependentSets.GeometryNames.levelExpr line 127
  10. lemma OAI.LargeIndependentSets.GeometryNames.levelExpr_eval line 130
  11. def OAI.LargeIndependentSets.GeometryNames.sameQuestionExpr line 135
  12. lemma OAI.LargeIndependentSets.GeometryNames.sameQuestionExpr_nonzero line 142
  13. def OAI.LargeIndependentSets.GeometryNames.copyCostExpr line 165
  14. lemma OAI.LargeIndependentSets.GeometryNames.copyCostExpr_eval line 170
  15. def OAI.LargeIndependentSets.GeometryNames.costExpr line 180
  16. lemma OAI.LargeIndependentSets.GeometryNames.costExpr_eval line 184