OAI/Combinatorics/KMedian/Programs/MaskBestProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Completion.Rational.BestProgram.card line 14
  2. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.card_poly line 15
  3. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.card_view line 16
  4. def OAI.MetricKMedian.Completion.Rational.BestProgram.good line 19
  5. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.good_poly line 20
  6. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.good_view line 21
  7. def OAI.MetricKMedian.Completion.Rational.BestProgram.annotate line 25
  8. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.annotate_poly line 27
  9. def OAI.MetricKMedian.Completion.Rational.BestProgram.raw line 29
  10. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.raw_poly line 30
  11. theorem OAI.MetricKMedian.Completion.Rational.BestProgram.raw_best line 31