OAI/Combinatorics/KMedian/Process/BatchActionList.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.RationalBatchData.ActionList.Raw line 14
  2. def OAI.MetricKMedian.RationalBatchData.ActionList.view line 16
  3. def OAI.MetricKMedian.RationalBatchData.ActionList.parent line 18
  4. def OAI.MetricKMedian.RationalBatchData.ActionList.child line 19
  5. def OAI.MetricKMedian.RationalBatchData.ActionList.valid line 20
  6. def OAI.MetricKMedian.RationalBatchData.ActionList.units line 24
  7. def OAI.MetricKMedian.RationalBatchData.ActionList.codes line 26
  8. theorem OAI.MetricKMedian.RationalBatchData.ActionList.parent_poly line 28
  9. theorem OAI.MetricKMedian.RationalBatchData.ActionList.child_poly line 29
  10. theorem OAI.MetricKMedian.RationalBatchData.ActionList.valid_poly line 30
  11. theorem OAI.MetricKMedian.RationalBatchData.ActionList.units_poly line 31
  12. theorem OAI.MetricKMedian.RationalBatchData.ActionList.codes_poly line 39
  13. theorem OAI.MetricKMedian.RationalBatchData.ActionList.units_length line 41
  14. theorem OAI.MetricKMedian.RationalBatchData.ActionList.parent_code line 45
  15. theorem OAI.MetricKMedian.RationalBatchData.ActionList.child_code line 56
  16. theorem OAI.MetricKMedian.RationalBatchData.ActionList.valid_code line 62
  17. theorem OAI.MetricKMedian.RationalBatchData.ActionList.mem_codes line 81
  18. theorem OAI.MetricKMedian.RationalBatchData.ActionList.codes_eq line 105