OAI/Combinatorics/KMedianRecovery/Encoding/LabelMember.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.eq line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.eq_computes line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.fields_injective line 18
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.eq_pair line 21
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.contains line 25
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.contains_computes line 26
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.contains_encode line 29
  8. theorem OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.encode_injective line 39
  9. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.subtypeList_values line 48
  10. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.filter_finRange line 53
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.lookup_list line 63
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.indices_list line 67
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.alphabet line 79
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.target line 80
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.index line 81
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.alphabet_computes line 82
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.target_computes line 83
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.index_computes line 84
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.test line 85
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.test_computes line 87
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.test_pack line 90
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.run line 96
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.run_computes line 98
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabelSelect.run_pack line 100