OAI/Combinatorics/KMedian/Rounding/GridDataProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.Input line 17
2. abbrev OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.Raw line 24
3. def OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.Input.raw line 25
4. abbrev OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.Input.encode line 27
5. def OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.Input.selection line 29
6. def OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.prepare line 39
7. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.prepare_poly line 42
8. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.prepare_input line 47
9. def OAI.MetricKMedian.FixedBatch.RationalParameters.GridDataProgram.program line 50