OAI/Combinatorics/KMedian/Hardness/Coverage.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Complexity.ManyOneReduces line 12
  2. structure OAI.MetricKMedian.Coverage.Input line 22
  3. def OAI.MetricKMedian.Coverage.Input.encode line 33
  4. def OAI.MetricKMedian.Coverage.Input.covered line 37
  5. def OAI.MetricKMedian.Coverage.Input.Perfect line 40
  6. def OAI.MetricKMedian.Coverage.Input.Sound line 43
  7. abbrev OAI.MetricKMedian.Coverage.Input.Point line 47
  8. def OAI.MetricKMedian.Coverage.Input.pointDistance line 49
  9. theorem OAI.MetricKMedian.Coverage.Input.pointDistance_nonneg line 55
  10. theorem OAI.MetricKMedian.Coverage.Input.pointDistance_eq_zero line 59
  11. theorem OAI.MetricKMedian.Coverage.Input.pointDistance_symm line 63
  12. theorem OAI.MetricKMedian.Coverage.Input.pointDistance_triangle line 67
  13. def OAI.MetricKMedian.Coverage.Input.client line 72
  14. def OAI.MetricKMedian.Coverage.Input.facility line 75
  15. theorem OAI.MetricKMedian.Coverage.Input.client_injective line 78
  16. theorem OAI.MetricKMedian.Coverage.Input.facility_injective line 82
  17. theorem OAI.MetricKMedian.Coverage.Input.client_ne_facility line 86
  18. def OAI.MetricKMedian.Coverage.Input.chosenFacilities line 92
  19. theorem OAI.MetricKMedian.Coverage.Input.chosenFacilities_card line 95
  20. theorem OAI.MetricKMedian.Coverage.Input.chosenFacilities_nonempty line 99
  21. def OAI.MetricKMedian.Coverage.Input.toMedian line 102
  22. theorem OAI.MetricKMedian.Coverage.Input.distance_client_facility line 115
  23. theorem OAI.MetricKMedian.Coverage.Input.chosenFacilities_subset line 120
  24. theorem OAI.MetricKMedian.Coverage.Input.mem_covered line 124
  25. theorem OAI.MetricKMedian.Coverage.Input.nearest_chosen_ge_one line 128
  26. theorem OAI.MetricKMedian.Coverage.Input.nearest_chosen line 137
  27. theorem OAI.MetricKMedian.Coverage.Input.cost_chosen line 154
  28. def OAI.MetricKMedian.Coverage.Input.selected line 176
  29. theorem OAI.MetricKMedian.Coverage.Input.chosen_selected line 179
  30. theorem OAI.MetricKMedian.Coverage.Input.selected_chosen line 190
  31. theorem OAI.MetricKMedian.Coverage.Input.cost_selected line 200
  32. theorem OAI.MetricKMedian.Coverage.Input.covered_card_le line 207
  33. theorem OAI.MetricKMedian.Coverage.Input.cost_ge_universe line 211
  34. theorem OAI.MetricKMedian.Coverage.Input.perfect_nonempty line 219
  35. theorem OAI.MetricKMedian.Coverage.Input.optimum_of_perfect line 226
  36. theorem OAI.MetricKMedian.Coverage.Input.cost_of_sound line 242
  37. def OAI.MetricKMedian.Coverage.GapNPReductions line 257