OAI/Combinatorics/KMedianRecovery/Recovery/OrderedMaximum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.OrderedMaximum.run line 8
  2. lemma OAI.MetricKMedianRecovery.OrderedMaximum.mem line 11
  3. lemma OAI.MetricKMedianRecovery.OrderedMaximum.own_le line 22
  4. lemma OAI.MetricKMedianRecovery.OrderedMaximum.score_le line 32
  5. lemma OAI.MetricKMedianRecovery.OrderedMaximum.fold line 42
  6. def OAI.MetricKMedianRecovery.OrderedMaximum.ofList line 47
  7. lemma OAI.MetricKMedianRecovery.OrderedMaximum.ofList_mem line 48
  8. lemma OAI.MetricKMedianRecovery.OrderedMaximum.le_ofList line 53
  9. lemma OAI.MetricKMedianRecovery.OrderedMaximum.cast_run line 61
  10. def OAI.MetricKMedianRecovery.Categorical.Selected.bag line 71
  11. lemma OAI.MetricKMedianRecovery.Categorical.Selected.bag_ne_nil line 73
  12. def OAI.MetricKMedianRecovery.Categorical.Selected.orderedRule line 80