OAI/Combinatorics/KMedianRecovery/Geometry/MetricAnchor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.pack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.rectInput line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.rectInput_computes line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.rectangle line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.rectangle_computes line 21
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.anchorInput line 22
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.anchorInput_computes line 25
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.run line 30
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.run_computes line 31
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.rectInput_pack line 34
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.rectangle_pack line 39
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.anchorInput_pack line 43
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMetricAnchor.produce line 50