OAI/Combinatorics/KMedianRecovery/Recovery/Pack10.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.pack line 11
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.resultBits line 18
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.run_eq line 23
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.resultBits_eq_nil_iff line 36
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.nil_iff line 40
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.witness line 50
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningOracle.row_count line 63