OAI/Combinatorics/IndependentSets/Encoding/GeometryExpr.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LargeIndependentSets.GeometryNames.staticCount line 14
  2. abbrev OAI.LargeIndependentSets.GeometryNames.size line 15
  3. lemma OAI.LargeIndependentSets.GeometryNames.staticCount_pos line 17
  4. lemma OAI.LargeIndependentSets.GeometryNames.size_pos line 20
  5. def OAI.LargeIndependentSets.GeometryNames.sizeExpr line 23
  6. def OAI.LargeIndependentSets.GeometryNames.pointExpr line 24
  7. def OAI.LargeIndependentSets.GeometryNames.uExpr line 25
  8. def OAI.LargeIndependentSets.GeometryNames.vExpr line 30
  9. lemma OAI.LargeIndependentSets.GeometryNames.sizeExpr_eval line 35
  10. lemma OAI.LargeIndependentSets.GeometryNames.uExpr_eval line 38
  11. lemma OAI.LargeIndependentSets.GeometryNames.vExpr_eval line 43
  12. lemma OAI.LargeIndependentSets.GeometryNames.pointExpr_eval line 48
  13. def OAI.LargeIndependentSets.GeometryNames.sameQuestion line 57
  14. lemma OAI.LargeIndependentSets.GeometryNames.sameQuestion_iff line 62