OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationChosenMasks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact subset unions behind the chosen stream occurrences

  1. def OAI.LowSpaceSubsetSum.RepresentationSetup.leafMask line 13
  2. def OAI.LowSpaceSubsetSum.RepresentationSetup.maskFirstChild line 16
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.firstTop_eq_block_union line 21
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.localBlocks_union line 44
  5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.localMask_blocks_union line 62
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskFirstChild_parts line 69
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskFirstChild_eq line 82
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosen_first_children_eq line 97