OAI/Combinatorics/IndependentSets/Geometry/GeometryDistance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.GeometryNames.distances line 16
  2. def OAI.LargeIndependentSets.GeometryNames.distanceComputer line 18
  3. lemma OAI.LargeIndependentSets.GeometryNames.distanceComputer_finiteAlphabet line 21
  4. lemma OAI.LargeIndependentSets.GeometryNames.enat_eighth line 25
  5. lemma OAI.LargeIndependentSets.GeometryNames.distance_threshold line 33
  6. abbrev OAI.LargeIndependentSets.GeometryNames.prefixCount line 43
  7. def OAI.LargeIndependentSets.GeometryNames.payloadOffsetExpr line 45
  8. def OAI.LargeIndependentSets.GeometryNames.fromTable line 49
  9. lemma OAI.LargeIndependentSets.GeometryNames.distances_suffix line 51
  10. lemma OAI.LargeIndependentSets.GeometryNames.payloadOffsetExpr_eval line 69
  11. lemma OAI.LargeIndependentSets.GeometryNames.fromTable_eval line 81
  12. lemma OAI.LargeIndependentSets.GeometryNames.cellExpr_eval line 85
  13. def OAI.LargeIndependentSets.GeometryNames.closeExpr line 94
  14. lemma OAI.LargeIndependentSets.GeometryNames.closeExpr_nonzero line 96