OAI/Combinatorics/KMedian/Process/CopyNearestProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.distances line 20
2. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.distances_poly line 21
3. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.distances_view line 22
4. def OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.nearestRaw line 31
5. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.nearestRaw_poly line 33
6. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.nearestRaw_view line 34
7. def OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.radiusRaw line 40
8. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.radiusRaw_poly line 42
9. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.CopyNearestProgram.radiusRaw_view line 43