OAI/Combinatorics/KMedianRecovery/Recovery/FiniteContext.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.labels line 11
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.setBits line 12
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.pack line 13
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.alphabet line 17
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.alphabet_computes line 19
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.alphabet_pack line 21
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.selected line 32
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.selected_computes line 34
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.selected_pack line 36
10. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.matrix line 52
11. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.matrix_computes line 55
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.matrix_pack line 57
13. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.run line 65
14. def OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.run_computes line 68
15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.run_pack line 75