OAI/Combinatorics/KMedianRecovery/Geometry/Nearest.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalOpenability.nearest line 11
  2. lemma OAI.MetricKMedianRecovery.RationalOpenability.nearest_cast line 15
  3. inductive OAI.MetricKMedianRecovery.RationalOpenability.Kind line 35
  4. abbrev OAI.MetricKMedianRecovery.RationalOpenability.Variables line 46
  5. def OAI.MetricKMedianRecovery.RationalOpenability.bid line 48
  6. def OAI.MetricKMedianRecovery.RationalOpenability.slack line 51
  7. def OAI.MetricKMedianRecovery.RationalOpenability.paymentForm line 56
  8. def OAI.MetricKMedianRecovery.RationalOpenability.dualForm line 64
  9. def OAI.MetricKMedianRecovery.RationalOpenability.system line 71
  10. lemma OAI.MetricKMedianRecovery.RationalOpenability.bid_eval line 84
  11. lemma OAI.MetricKMedianRecovery.RationalOpenability.slack_eval line 88
  12. lemma OAI.MetricKMedianRecovery.RationalOpenability.payment_eval line 94
  13. lemma OAI.MetricKMedianRecovery.RationalOpenability.dual_eval line 112
  14. lemma OAI.MetricKMedianRecovery.RationalOpenability.system_iff line 125
  15. theorem OAI.MetricKMedianRecovery.RationalOpenability.rational_openable line 200