OAI/Combinatorics/KMedian/Programs/RestrictionProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Reduction.Enumeration.list_toFinset_map line 16
  2. theorem OAI.MetricKMedian.Reduction.Enumeration.choices_eq_of_mem line 18
  3. def OAI.MetricKMedian.Reduction.Enumeration.choices line 31
  4. theorem OAI.MetricKMedian.Reduction.Enumeration.mem_orderList line 33
  5. theorem OAI.MetricKMedian.Reduction.Enumeration.choices_toFinset line 40
  6. theorem OAI.MetricKMedian.Reduction.Enumeration.choicesRaw_choices line 42
  7. def OAI.MetricKMedian.Reduction.Enumeration.arcpairs line 45
  8. theorem OAI.MetricKMedian.Reduction.Enumeration.arcpairs_poly line 48
  9. def OAI.MetricKMedian.Reduction.Enumeration.pairs line 49
  10. theorem OAI.MetricKMedian.Reduction.Enumeration.arcpairs_view line 51
  11. theorem OAI.MetricKMedian.Reduction.Enumeration.pairs_mem line 58
  12. def OAI.MetricKMedian.Reduction.Enumeration.restrictData line 64
  13. theorem OAI.MetricKMedian.Reduction.Enumeration.restrictData_poly line 68
  14. theorem OAI.MetricKMedian.Reduction.Enumeration.restrictData_view line 75
  15. def OAI.MetricKMedian.Reduction.Enumeration.branches line 84
  16. theorem OAI.MetricKMedian.Reduction.Enumeration.branches_toFinset line 86
  17. def OAI.MetricKMedian.Reduction.Enumeration.branchesData line 91
  18. theorem OAI.MetricKMedian.Reduction.Enumeration.branchesData_poly line 93
  19. theorem OAI.MetricKMedian.Reduction.Enumeration.branchesData_view line 94