OAI/Combinatorics/KMedian/Hardness/ProjectionInput.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.covered_iff line 19
  2. structure OAI.MetricKMedian.Coverage.ProjectionInput line 25
  3. def OAI.MetricKMedian.Coverage.ProjectionInput.Perfect line 41
  4. def OAI.MetricKMedian.Coverage.ProjectionInput.Sound line 44
  5. abbrev OAI.MetricKMedian.Coverage.ProjectionInput.Block line 47
  6. def OAI.MetricKMedian.Coverage.ProjectionInput.width line 48
  7. def OAI.MetricKMedian.Coverage.ProjectionInput.blockEquiv line 50
  8. def OAI.MetricKMedian.Coverage.ProjectionInput.clientEquiv line 53
  9. abbrev OAI.MetricKMedian.Coverage.ProjectionInput.facilityEquiv line 58
  10. abbrev OAI.MetricKMedian.Coverage.ProjectionInput.toCoverage line 60
  11. theorem OAI.MetricKMedian.Coverage.ProjectionInput.incident_equiv line 73
  12. theorem OAI.MetricKMedian.Coverage.ProjectionInput.covered_equiv line 81
  13. theorem OAI.MetricKMedian.Coverage.ProjectionInput.coverage_perfect line 111
  14. theorem OAI.MetricKMedian.Coverage.ProjectionInput.coverage_sound line 122