OAI/Combinatorics/KMedianRecovery/Recovery/Form.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form line 8
  2. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.eval line 15
  3. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval line 16
  4. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.const line 19
  5. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.coord line 20
  6. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.add line 21
  7. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.sub line 22
  8. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.sum line 23
  9. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.eval_const line 25
  10. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval_const line 26
  11. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.eval_coord line 27
  12. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval_coord line 28
  13. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.eval_add line 29
  14. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval_add line 32
  15. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.eval_sub line 35
  16. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval_sub line 38
  17. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.eval_sum line 41
  18. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval_sum line 45
  19. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.realEval_cast line 50
  20. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.toRow line 53
  21. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.toRow_realHolds line 56
  22. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Form.toRow_holds line 62
  23. theorem OAI.MetricKMedianRecovery.RationalLinearFeasibility.affine_rational_witness line 72