OAI/Combinatorics/KMedianRecovery/Recovery/FinImages.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.table line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.sort_list line 10
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.sort_table line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.image line 25
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.image_computes line 26
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.image_list line 27
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.image_ofFn line 37
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.image_pack line 46
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.bottom_pack line 49
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.encode_lengthBits line 55
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.left line 62
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.right line 63
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.left_encode line 64
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.plus line 67
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.plus_computes line 68
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.shift line 69
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.shift_computes line 70
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.shift_encode line 71
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.minus line 82
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.minus_computes line 83
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.unshift line 84
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.unshift_computes line 85
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.unshift_encode line 86
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryTaggedSets.disjoint line 103