OAI/Combinatorics/KMedian/Reduction/DeletionHistory.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.deletionValues line 12
  2. theorem OAI.MetricKMedian.Reduction.deletion_value_mem line 16
  3. theorem OAI.MetricKMedian.Reduction.card_deletionValues line 27
  4. def OAI.MetricKMedian.Reduction.eligible line 37
  5. def OAI.MetricKMedian.Reduction.deleteStep line 41
  6. theorem OAI.MetricKMedian.Reduction.deleteStep_cases line 46
  7. theorem OAI.MetricKMedian.Reduction.deleteStep_subset line 57
  8. theorem OAI.MetricKMedian.Reduction.deleteStep_card line 63
  9. theorem OAI.MetricKMedian.Reduction.deleteStep_congr line 69
  10. def OAI.MetricKMedian.Reduction.deletionHistory line 82
  11. theorem OAI.MetricKMedian.Reduction.history_bounds line 87
  12. theorem OAI.MetricKMedian.Reduction.enumerate_ideal_history line 97