OAI/Combinatorics/KMedianRecovery/Recovery/Op2.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.op line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.op_computes line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.operation_eq line 12
  4. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.fold_eq line 15
  5. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.length_flatten_le line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.run line 24
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.run_computes line 25
  8. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.run_encode line 28
  9. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Flatten.encode_flatMap line 38
  10. def OAI.MetricKMedianRecovery.BitMachine.WordList.flatMapWith line 44
  11. def OAI.MetricKMedianRecovery.BitMachine.WordList.flatMapWith_computes line 45
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.flatMapWith_encode line 47
  13. def OAI.MetricKMedianRecovery.BitMachine.WordList.crossWith line 59
  14. def OAI.MetricKMedianRecovery.BitMachine.WordList.crossWith_computes line 62
  15. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.crossWith_encode line 73
  16. def OAI.MetricKMedianRecovery.BitMachine.WordList.cross line 81
  17. def OAI.MetricKMedianRecovery.BitMachine.WordList.cross_computes line 82
  18. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.cross_encode line 83
  19. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.flatMap_ofFn line 92
  20. def OAI.MetricKMedianRecovery.BitMachine.WordList.map line 97
  21. def OAI.MetricKMedianRecovery.BitMachine.WordList.map_computes line 99
  22. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.map_encode line 105
  23. def OAI.MetricKMedianRecovery.BitMachine.WordList.list_computes line 108
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.clients line 116
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.clients_computes line 117
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.doubles line 118
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.doubles_computes line 119
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.triples line 120
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.triples_computes line 121
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.caps line 122
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.caps_computes line 123
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.duals line 124
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.duals_computes line 125
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.unaryTag line 127
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.unaryTag_computes line 128
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.pairTag line 130
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.pairTag_computes line 131
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.tripleTag line 134
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.tripleTag_computes line 136
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.dualTag line 140
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.dualTag_computes line 141
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.variableTag line 144
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.variableTag_computes line 146
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.kinds line 150
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.kinds_computes line 155
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.columns line 166
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.columns_computes line 168
  48. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.clients_pack line 174
  49. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.kinds_pack line 179
  50. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningEnumeration.columns_pack line 189