OAI/Combinatorics/KMedian/Programs/BoundedEnumerationProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.Enumeration.words line 13
  2. theorem OAI.MetricKMedian.Reduction.Enumeration.words_poly line 16
  3. theorem OAI.MetricKMedian.Reduction.Enumeration.mem_words line 30
  4. theorem OAI.MetricKMedian.Reduction.Enumeration.choices_eq line 51
  5. def OAI.MetricKMedian.Reduction.Enumeration.maskWord line 63
  6. theorem OAI.MetricKMedian.Reduction.Enumeration.maskWord_poly line 64
  7. theorem OAI.MetricKMedian.Reduction.Enumeration.maskWord_view line 70
  8. theorem OAI.MetricKMedian.Reduction.Enumeration.words_map line 82
  9. def OAI.MetricKMedian.Reduction.Enumeration.choicesRaw line 88
  10. theorem OAI.MetricKMedian.Reduction.Enumeration.choicesRaw_poly line 90
  11. theorem OAI.MetricKMedian.Reduction.Enumeration.choicesRaw_view line 91