OAI/Combinatorics/KMedianRecovery/Encoding/RationalBottomIndices.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.indexSet line 8
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.indexSet_image line 10
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.indexSet_card line 20
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.indexSet_sum line 23
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.rawIndices line 34
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.rawIndices_computes line 36
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottomIndices line 42
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.bottomIndices_finset line 44
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRationalSort.rawIndices_pack line 52