OAI/Combinatorics/KMedianRecovery/Recovery/RecoveryCandidates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.positive line 12
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zero line 16
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.candidates line 19
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.result line 23
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.zero_mem line 25
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.positive_mem line 27
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.candidates_property line 31
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.result_property line 43
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.run_source line 48