OAI/Combinatorics/KMedianRecovery/Recovery/FilterItem.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.filterItem line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.WordList.filterItem_computes line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.WordList.filterWith line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.WordList.filterWith_computes line 18
  5. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.filterWith_encode line 20
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.canonical_list line 32
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.old line 44
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.old_computes line 45
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.new line 46
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.new_computes line 47
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.keep line 48
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.keep_computes line 50
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.keep_pack line 56
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.run line 62
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.run_computes line 63
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteInsert.run_pack line 64