OAI/Combinatorics/KMedianRecovery/Recovery/ClassFilter.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.pack line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.tag line 12
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.tag_computes line 13
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.matching line 15
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.matching_computes line 16
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.run line 18
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.run_computes line 19
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryClassFilter.run_pack line 20