OAI/Combinatorics/KMedianRecovery/Encoding/RationalSort.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.entryBits line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.lt line 10
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.lt_computes line 14
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.lt_pack line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sort line 23
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sort_computes line 24
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.sort_pack line 25
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.ranked line 28
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.ranked_computes line 31
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.ranking line 36
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.ranked_pack line 37
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottom line 42
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottom_computes line 44
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottom_pack line 46
  15. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.pack line 56
  16. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.encode line 57
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.lt line 58
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.lt_computes line 59
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.lt_pack line 60
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.sort line 62
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.sort_computes line 63
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.sort_pack line 64
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.union line 65
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.union_computes line 66
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.union_pack line 67
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.contains line 70
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.contains_computes line 71
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.contains_pack line 72
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.absent line 79
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.absent_computes line 80
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.diff line 82
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.diff_computes line 83
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.diff_pack line 85
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.union_encode line 92
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNatSet.diff_encode line 94