OAI/Combinatorics/KMedian/Programs/BundlesProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseBundles.Program.qr line 14
  2. abbrev OAI.MetricKMedian.SparseBundles.Program.qt line 15
  3. abbrev OAI.MetricKMedian.SparseBundles.Program.eqi line 16
  4. structure OAI.MetricKMedian.SparseBundles.Program.QInput line 18
  5. def OAI.MetricKMedian.SparseBundles.Program.QInput.raw line 24
  6. abbrev OAI.MetricKMedian.SparseBundles.Program.QInput.encode line 26
  7. def OAI.MetricKMedian.SparseBundles.Program.QInput.column line 28
  8. def OAI.MetricKMedian.SparseBundles.Program.QInput.columns line 30
  9. def OAI.MetricKMedian.SparseBundles.Program.emptyColumn line 31
  10. def OAI.MetricKMedian.SparseBundles.Program.QInput.input line 32
  11. def OAI.MetricKMedian.SparseBundles.Program.QInput.result line 33
  12. def OAI.MetricKMedian.SparseBundles.Program.columnsProgram line 37
  13. def OAI.MetricKMedian.SparseBundles.Program.inputProgram line 45
  14. def OAI.MetricKMedian.SparseBundles.Program.lawProgram line 53