OAI/Combinatorics/KMedianRecovery/Branching/BranchBalls.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.filter_sort line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.pack line 20
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.row line 22
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.row_computes line 24
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.input line 26
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.input_computes line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.ball line 30
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.ball_computes line 31
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.ball_pair line 32
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.balls line 38
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.balls_computes line 39
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.balls_pack line 43
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.run line 48
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.run_computes line 49
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchBalls.run_pack line 51