OAI/Combinatorics/KMedianRecovery/Recovery/FiniteContinuation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.alphabet line 11
  2. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.mem_alphabet line 14
  3. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.alphabet_nodup line 19
  4. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.alphabet_length line 22
  5. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.embed line 31
  6. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.index line 39
  7. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.embed_index line 42
  8. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.located line 45
  9. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.embed_located line 48
  10. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.select line 51
  11. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.mem_select line 54
  12. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.image_select line 57
  13. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.select_cover line 67
  14. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.metric line 73
  15. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.rows line 77
  16. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.complete line 80
  17. def OAI.MetricKMedianRecovery.FiniteLabelContinuation.continuation line 85
  18. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.complete_spec line 92
  19. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.continuation_spec line 130
  20. theorem OAI.MetricKMedianRecovery.FiniteLabelContinuation.correct_completion line 164