OAI/Combinatorics/KMedianRecovery/Encoding/WordSubsets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.update line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.fold_from line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.fold_empty line 19
  4. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.addLast line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.addLast_computes line 21
  6. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.added line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.added_computes line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.op line 28
  9. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.op_computes line 29
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.op_pack line 30
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.length_encode_sublist line 34
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.encode_bound line 39
  13. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.subset_bound line 48
  14. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.prefix_bound line 55
  15. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.cap line 62
  16. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.run line 63
  17. def OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.run_computes line 65
  18. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Subsets.run_pack line 68