OAI/Combinatorics/KMedian/Compression/ComputedPivot.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.IntegerLaw.positiveSet line 9
  2. theorem OAI.MetricKMedian.IntegerLaw.positiveSet_nonempty line 12
  3. def OAI.MetricKMedian.IntegerLaw.ratio line 17
  4. def OAI.MetricKMedian.IntegerLaw.leastRatio line 20
  5. def OAI.MetricKMedian.IntegerLaw.pivotSet line 24
  6. theorem OAI.MetricKMedian.IntegerLaw.pivotSet_nonempty line 28
  7. def OAI.MetricKMedian.IntegerLaw.computedPivot line 34
  8. theorem OAI.MetricKMedian.IntegerLaw.computedPivot_spec line 38
  9. theorem OAI.MetricKMedian.IntegerLaw.updated_nonneg line 49
  10. def OAI.MetricKMedian.IntegerLaw.eliminateAt line 63
  11. theorem OAI.MetricKMedian.IntegerLaw.eliminateAt_numerator line 78