OAI/Combinatorics/KMedianRecovery/Recovery/Row.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row line 7
  2. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.value line 11
  3. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.realValue line 12
  4. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.Holds line 15
  5. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.RealHolds line 16
  6. instance OAI.MetricKMedianRecovery.RationalLinearFeasibility.(instance at line 17) line 17
  7. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.head line 19
  8. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.tail line 20
  9. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.combine line 22
  10. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.value_cons line 25
  11. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.realValue_cons line 29
  12. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.combine_value line 33
  13. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.combine_realValue line 37
  14. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.Row.realHolds_cast line 42
  15. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.eliminate line 48
  16. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.eliminate_sound line 53
  17. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.boundary line 77
  18. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.lowers line 80
  19. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.uppers line 82
  20. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.pick line 85
  21. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.le_foldr_max line 87
  22. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.foldr_min_le line 95
  23. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.foldr_max_le line 103
  24. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.pick_spec line 109
  25. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.boundary_order line 117
  26. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.eliminate_complete line 129
  27. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.solve line 157
  28. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.solve_sound line 161
  29. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.solve_complete line 174
  30. theorem OAI.MetricKMedianRecovery.RationalLinearFeasibility.rational_witness line 192