OAI/Combinatorics/KMedian/Process/BatchProposalProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input line 17
  2. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input.raw line 32
  3. abbrev OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input.encode line 34
  4. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input.enumActions line 36
  5. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input.batch line 37
  6. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input.law line 45
  7. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.Input.result line 46
  8. theorem OAI.MetricKMedian.RationalBatchData.ProposalProgram.data_input line 50
  9. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.inputProgram line 54
  10. theorem OAI.MetricKMedian.RationalBatchData.ProposalProgram.result_eq line 57
  11. def OAI.MetricKMedian.RationalBatchData.ProposalProgram.program line 72