OAI/Combinatorics/KMedian/Binary/BinaryBooleanLists.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Binary.BooleanLists.pack line 12
2. theorem OAI.MetricKMedian.Binary.BooleanLists.pack_run line 17
3. inductive OAI.MetricKMedian.Binary.BooleanLists.Phase line 21
4. instance OAI.MetricKMedian.Binary.BooleanLists.(instance at line 22) line 22
5. def OAI.MetricKMedian.Binary.BooleanLists.unpack line 23
6. theorem OAI.MetricKMedian.Binary.BooleanLists.unpack_run line 31
7. def OAI.MetricKMedian.Binary.BooleanLists.packProgram line 35
8. def OAI.MetricKMedian.Binary.BooleanLists.unpackProgram line 37
9. def OAI.MetricKMedian.Binary.BooleanLists.valueProgram line 39
10. theorem OAI.MetricKMedian.Binary.BooleanLists.length line 40