OAI/Combinatorics/KMedian/Programs/RationalSortProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.RationalSortProgram.insertData line 12
  2. theorem OAI.MetricKMedian.RationalSortProgram.insertData_poly line 14
  3. theorem OAI.MetricKMedian.RationalSortProgram.filters_length line 20
  4. theorem OAI.MetricKMedian.RationalSortProgram.insertData_length line 34
  5. def OAI.MetricKMedian.RationalSortProgram.sort line 42
  6. def OAI.MetricKMedian.RationalSortProgram.foldProgram line 43
  7. theorem OAI.MetricKMedian.RationalSortProgram.sort_poly line 46
  8. theorem OAI.MetricKMedian.RationalSortProgram.insertData_sorted line 49
  9. theorem OAI.MetricKMedian.RationalSortProgram.insertData_mem line 60
  10. theorem OAI.MetricKMedian.RationalSortProgram.insertData_sort line 67
  11. theorem OAI.MetricKMedian.RationalSortProgram.fold_sort line 73
  12. theorem OAI.MetricKMedian.RationalSortProgram.sort_eq line 83