OAI/Combinatorics/KMedian/Programs/InstanceZeroProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.InstanceProgram.subsetRaw line 16
  2. theorem OAI.MetricKMedian.InstanceProgram.subsetRaw_poly line 17
  3. theorem OAI.MetricKMedian.InstanceProgram.subsetRaw_view line 21
  4. def OAI.MetricKMedian.InstanceProgram.zeroTestData line 34
  5. theorem OAI.MetricKMedian.InstanceProgram.zeroTestData_poly line 35
  6. theorem OAI.MetricKMedian.InstanceProgram.zeroTestData_view line 36
  7. def OAI.MetricKMedian.InstanceProgram.zeroTestProgram line 40
  8. def OAI.MetricKMedian.InstanceProgram.first line 43
  9. theorem OAI.MetricKMedian.InstanceProgram.first_poly line 44
  10. theorem OAI.MetricKMedian.InstanceProgram.first_view line 45
  11. def OAI.MetricKMedian.InstanceProgram.singletonRaw line 55
  12. theorem OAI.MetricKMedian.InstanceProgram.singletonRaw_poly line 56
  13. theorem OAI.MetricKMedian.InstanceProgram.singletonRaw_view line 57
  14. def OAI.MetricKMedian.InstanceProgram.singletonData line 59
  15. theorem OAI.MetricKMedian.InstanceProgram.singletonData_poly line 60
  16. theorem OAI.MetricKMedian.InstanceProgram.singletonData_view line 61
  17. def OAI.MetricKMedian.InstanceProgram.zeroOutputData line 64
  18. theorem OAI.MetricKMedian.InstanceProgram.zeroOutputData_poly line 65
  19. theorem OAI.MetricKMedian.InstanceProgram.zeroOutputData_view line 66
  20. def OAI.MetricKMedian.InstanceProgram.zeroOutputProgram line 74