OAI/Combinatorics/KMedianRecovery/Recovery/Entry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.PhaseSequence.Entry line 10
  2. inductive OAI.MetricKMedianRecovery.PhaseSequence.Prefix line 14
  3. def OAI.MetricKMedianRecovery.PhaseSequence.Maximal line 22
  4. def OAI.MetricKMedianRecovery.PhaseSequence.Valid line 25
  5. inductive OAI.MetricKMedianRecovery.PhaseHistoryTransfer.History line 33
  6. def OAI.MetricKMedianRecovery.PhaseHistoryTransfer.after line 40
  7. def OAI.MetricKMedianRecovery.PhaseMergeCompletion.Regular line 49
  8. def OAI.MetricKMedianRecovery.PhaseMergeCompletion.Attains line 51
  9. def OAI.MetricKMedianRecovery.RationalPhase.historyRun line 59
  10. lemma OAI.MetricKMedianRecovery.RationalPhase.historyRun_fst line 68
  11. lemma OAI.MetricKMedianRecovery.RationalPhase.finish_prefix line 75
  12. theorem OAI.MetricKMedianRecovery.RationalPhase.historyRun_spec line 113
  13. def OAI.MetricKMedianRecovery.RationalPhase.count line 162
  14. theorem OAI.MetricKMedianRecovery.RationalPhase.count_attains line 166