OAI/Combinatorics/KMedianRecovery/Geometry/MetricCost2.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.pack line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.connection line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.cost line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.near line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.near_computes line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.run line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.run_computes line 20
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.run_pack line 25
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.connection_cast line 39
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricCost.cost_cast line 63
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.score line 74
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.score_computes line 76
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.context line 81
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.score_pack line 83
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.best line 89
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.run line 91
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.run_computes line 92
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.run_pack line 93
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.best_mem line 97
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.cost_le_self line 99
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.cost_le_mem line 102
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.best_property line 106
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricBest.realCost_le_mem line 112