OAI/Combinatorics/KMedian/Process/BatchActionCodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.RationalBatchData.ActionCodes.pairOrder line 12
2. abbrev OAI.MetricKMedian.RationalBatchData.ActionCodes.actionOrder line 14
3. def OAI.MetricKMedian.RationalBatchData.ActionCodes.code line 18
4. theorem OAI.MetricKMedian.RationalBatchData.ActionCodes.code_strictMono line 22
5. theorem OAI.MetricKMedian.RationalBatchData.ActionCodes.code_lt line 54
6. def OAI.MetricKMedian.RationalBatchData.ActionCodes.valid line 63
7. theorem OAI.MetricKMedian.RationalBatchData.ActionCodes.valid_iff line 67
8. theorem OAI.MetricKMedian.RationalBatchData.ActionCodes.enumeration_strictMono line 83