OAI/Combinatorics/LowSpaceSubsetSum/Storage/CoordinateRowCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Sorting and retaining one concrete separator coordinate row

  1. def OAI.LowSpaceSubsetSum.CoordinateRowCells.sorted line 12
  2. theorem OAI.LowSpaceSubsetSum.CoordinateRowCells.sorted_value line 15
  3. def OAI.LowSpaceSubsetSum.CoordinateRowCells.run line 18
  4. theorem OAI.LowSpaceSubsetSum.CoordinateRowCells.value line 23
  5. theorem OAI.LowSpaceSubsetSum.CoordinateRowCells.cells line 27