OAI/Combinatorics/LowSpaceSubsetSum/Storage/CanonicalBackground.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The sorted outside domain from the remaining canonical interval

  1. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.in_three_intervals line 12
  2. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.raw_mem line 24
  3. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.union_mem line 38
  4. def OAI.LowSpaceSubsetSum.CanonicalBackground.run line 59
  5. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.domain_eq line 62
  6. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.value line 78
  7. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.work line 85
  8. theorem OAI.LowSpaceSubsetSum.CanonicalBackground.length_le line 88