OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationTopCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete representation layout in the separator's coordinates

  1. def OAI.LowSpaceSubsetSum.RepresentationSetup.topCoordinates line 14
  2. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.topCoordinates_domain line 20
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawEntry_local_count line 25
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.collected_local_count line 42