OAI/Combinatorics/KMedianRecovery/Recovery/EnumeratedRow.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.enumeratedRow line 9
  2. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.enumeratedRow_realHolds line 12
  3. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.enumeratedRow_holds line 18
  4. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.solveForms line 26
  5. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.solveForms_sound line 29
  6. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.solveForms_complete line 37
  7. def OAI.MetricKMedianRecovery.EffectiveOpenability.active line 53
  8. instance OAI.MetricKMedianRecovery.EffectiveOpenability.activeDecidable line 55
  9. def OAI.MetricKMedianRecovery.EffectiveOpenability.bid line 58
  10. def OAI.MetricKMedianRecovery.EffectiveOpenability.slack line 59
  11. def OAI.MetricKMedianRecovery.EffectiveOpenability.payment line 61
  12. def OAI.MetricKMedianRecovery.EffectiveOpenability.dual line 67
  13. def OAI.MetricKMedianRecovery.EffectiveOpenability.forms line 71
  14. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.active_iff line 83
  15. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.bid_eq line 92
  16. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.slack_eq line 97
  17. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.forms_eq line 102
  18. def OAI.MetricKMedianRecovery.EffectiveOpenability.solveOpening line 120
  19. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.solveOpening_sound line 124
  20. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.solveOpening_complete line 135