OAI/Combinatorics/KMedian/Programs/InstanceDataProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.InstanceProgram.Matrix line 17
  2. abbrev OAI.MetricKMedian.InstanceProgram.Raw line 18
  3. def OAI.MetricKMedian.InstanceProgram.view line 19
  4. abbrev OAI.MetricKMedian.InstanceProgram.encode line 21
  5. def OAI.MetricKMedian.InstanceProgram.dcData line 22
  6. theorem OAI.MetricKMedian.InstanceProgram.dcData_poly line 23
  7. theorem OAI.MetricKMedian.InstanceProgram.dcData_view line 24
  8. def OAI.MetricKMedian.InstanceProgram.ddData line 28
  9. def OAI.MetricKMedian.InstanceProgram.dfData line 29
  10. theorem OAI.MetricKMedian.InstanceProgram.ddData_poly line 30
  11. theorem OAI.MetricKMedian.InstanceProgram.dfData_poly line 31
  12. theorem OAI.MetricKMedian.InstanceProgram.ddData_view line 32
  13. theorem OAI.MetricKMedian.InstanceProgram.dfData_view line 34
  14. abbrev OAI.MetricKMedian.InstanceProgram.Nonzero line 36
  15. abbrev OAI.MetricKMedian.InstanceProgram.nzEncode line 37
  16. def OAI.MetricKMedian.InstanceProgram.lpInput line 38
  17. def OAI.MetricKMedian.InstanceProgram.lpData line 41
  18. theorem OAI.MetricKMedian.InstanceProgram.lpData_poly line 42
  19. def OAI.MetricKMedian.InstanceProgram.lpProgram line 43
  20. def OAI.MetricKMedian.InstanceProgram.fractionalData line 46
  21. theorem OAI.MetricKMedian.InstanceProgram.fractionalData_poly line 48
  22. def OAI.MetricKMedian.InstanceProgram.fractionalInput line 50
  23. theorem OAI.MetricKMedian.InstanceProgram.fractionalData_view line 55
  24. def OAI.MetricKMedian.InstanceProgram.fractionalProgram line 59