OAI/Combinatorics/KMedianRecovery/Recovery/FiniteCross.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.FiniteLabelCrossing.run line 10
  2. theorem OAI.MetricKMedianRecovery.FiniteLabelCrossing.run_spec line 18
  3. inductive OAI.MetricKMedianRecovery.CanonicalLengthView.Plan line 60
  4. def OAI.MetricKMedianRecovery.CanonicalLengthView.Plan.root line 64
  5. def OAI.MetricKMedianRecovery.CanonicalLengthView.Plan.common line 68
  6. def OAI.MetricKMedianRecovery.CanonicalLengthView.Plan.small line 72
  7. def OAI.MetricKMedianRecovery.CanonicalLengthView.Plan.large line 76
  8. def OAI.MetricKMedianRecovery.CanonicalLengthView.accepts line 80
  9. instance OAI.MetricKMedianRecovery.CanonicalLengthView.(instance at line 84) line 84
  10. def OAI.MetricKMedianRecovery.CanonicalLengthView.candidates line 87
  11. def OAI.MetricKMedianRecovery.CanonicalLengthView.view line 90
  12. lemma OAI.MetricKMedianRecovery.CanonicalLengthView.candidates_length line 94
  13. lemma OAI.MetricKMedianRecovery.CanonicalLengthView.view_sound line 100
  14. lemma OAI.MetricKMedianRecovery.CanonicalLengthView.view_exists line 105