OAI/Combinatorics/KMedian/Reduction/Sparsification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.Reduction.nearest_triangle line 16
2. theorem OAI.MetricKMedian.Reduction.denseBall_cost line 22
3. theorem OAI.MetricKMedian.Reduction.denseBall_disjoint line 35
4. theorem OAI.MetricKMedian.Reduction.sparsify line 47