OAI/Combinatorics/KMedian/Programs/BranchProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Reduction.Program.Branch line 18
  2. def OAI.MetricKMedian.Reduction.Program.Branch.view line 22
  3. def OAI.MetricKMedian.Reduction.Program.Branch.encode line 23
  4. def OAI.MetricKMedian.Reduction.Program.Branch.allowed line 24
  5. instance OAI.MetricKMedian.Reduction.Program.Branch.(instance at line 25) line 25
  6. def OAI.MetricKMedian.Reduction.Program.Branch.restricted line 26
  7. def OAI.MetricKMedian.Reduction.Program.Branch.allowedProgram line 27
  8. def OAI.MetricKMedian.Reduction.Program.Branch.restrictedData line 32
  9. theorem OAI.MetricKMedian.Reduction.Program.Branch.restrictedData_poly line 33
  10. theorem OAI.MetricKMedian.Reduction.Program.Branch.restrictedData_view line 34
  11. def OAI.MetricKMedian.Reduction.Program.Branch.restrictedProgram line 35
  12. def OAI.MetricKMedian.Reduction.Program.branchOut line 42
  13. def OAI.MetricKMedian.Reduction.Program.goodProgram line 44
  14. def OAI.MetricKMedian.Reduction.Program.branchProgram line 51
  15. def OAI.MetricKMedian.Reduction.Program.branchList line 59
  16. def OAI.MetricKMedian.Reduction.Program.branchListProgram line 60
  17. def OAI.MetricKMedian.Reduction.Program.allList line 69
  18. theorem OAI.MetricKMedian.Reduction.Program.allList_toFinset line 71
  19. def OAI.MetricKMedian.Reduction.Program.allListProgram line 81