OAI/Combinatorics/KMedianRecovery/Geometry/NearestDistance.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.nearestDistance line 7
  2. def OAI.MetricKMedianRecovery.activeAt line 11
  3. def OAI.MetricKMedianRecovery.clippedAt line 15
  4. def OAI.MetricKMedianRecovery.bidRow line 19
  5. def OAI.MetricKMedianRecovery.admissibleBids line 23
  6. def OAI.MetricKMedianRecovery.openingPayment line 29
  7. def OAI.MetricKMedianRecovery.openingDual line 35
  8. def OAI.MetricKMedianRecovery.etaOpenable line 41
  9. lemma OAI.MetricKMedianRecovery.nearestDistance_nonneg line 47
  10. lemma OAI.MetricKMedianRecovery.nearestDistance_attained line 55
  11. lemma OAI.MetricKMedianRecovery.nearestDistance_le_mem line 61
  12. lemma OAI.MetricKMedianRecovery.nearestDistance_antitone line 68
  13. lemma OAI.MetricKMedianRecovery.activeAt_iff line 75
  14. lemma OAI.MetricKMedianRecovery.inactive_nonempty line 87
  15. lemma OAI.MetricKMedianRecovery.clippedAt_of_active line 95
  16. lemma OAI.MetricKMedianRecovery.clippedAt_of_inactive line 104
  17. lemma OAI.MetricKMedianRecovery.clippedAt_le_phase line 114
  18. lemma OAI.MetricKMedianRecovery.clippedAt_le_connection line 122
  19. lemma OAI.MetricKMedianRecovery.clippedAt_mono_phase line 132
  20. lemma OAI.MetricKMedianRecovery.clippedAt_antitone_open line 142
  21. lemma OAI.MetricKMedianRecovery.bidRow_antitone_open line 152
  22. lemma OAI.MetricKMedianRecovery.continuous_clippedAt line 159
  23. lemma OAI.MetricKMedianRecovery.continuous_bidRow line 168
  24. lemma OAI.MetricKMedianRecovery.bidRow_eq_zero_of_open line 175
  25. lemma OAI.MetricKMedianRecovery.inactive_at_later_phase line 186
  26. lemma OAI.MetricKMedianRecovery.capped_triangle_row line 194
  27. theorem OAI.MetricKMedianRecovery.crossing_openable line 213