OAI/Combinatorics/KMedianRecovery/Branching/CompletionFillMath.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Completion.Canonical.pick line 9
  2. lemma OAI.MetricKMedianRecovery.Completion.Canonical.pick_part line 12
  3. lemma OAI.MetricKMedianRecovery.Completion.Canonical.pick_covers line 20
  4. def OAI.MetricKMedianRecovery.Completion.Canonical.filled line 34
  5. lemma OAI.MetricKMedianRecovery.Completion.Canonical.filled_subset line 37
  6. lemma OAI.MetricKMedianRecovery.Completion.Canonical.filled_card line 43
  7. lemma OAI.MetricKMedianRecovery.Completion.Canonical.filled_covers line 45
  8. lemma OAI.MetricKMedianRecovery.Completion.Canonical.filled_ball line 51
  9. def OAI.MetricKMedianRecovery.Completion.Canonical.pad line 61
  10. lemma OAI.MetricKMedianRecovery.Completion.Canonical.subset_pad line 62
  11. lemma OAI.MetricKMedianRecovery.Completion.Canonical.pad_subset line 63
  12. lemma OAI.MetricKMedianRecovery.Completion.Canonical.pad_card line 65
  13. lemma OAI.MetricKMedianRecovery.Completion.Canonical.pad_nonempty line 74
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.pack line 81
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.need line 83
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.need_computes line 84
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.remaining line 85
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.remaining_computes line 86
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.run line 87
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.run_computes line 89
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.need_pack line 91
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.remaining_pack line 94
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionPad.run_pack line 97